[Merged by Bors] - feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas #18933

vihdzp · 2024-11-12T20:17:13Z

github-actions · 2024-11-12T20:18:00Z

PR summary 894c9e7d0b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ _root_.Equiv.lift_cardinal_eq
+ add_mk_eq_self
+ mk_congr_lift
+ mk_image_embedding
+ mk_image_embedding_lift
+ mk_preimage_equiv
+ mk_preimage_equiv_lift
+ mk_range_inl
+ mk_range_inr

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Mathlib/SetTheory/Cardinal/Basic.lean

b-mehta · 2024-12-15T23:19:58Z

Mathlib/SetTheory/Cardinal/Basic.lean

+theorem mk_preimage_equiv_lift {β : Type v} (f : α ≃ β) (s : Set β) :
+    lift.{v} #(f ⁻¹' s) = lift.{u} #s := by


Do we already have the image version of this too?

I've added these to the PR - note that the image version can be stated with just an embedding instead of an equiv.

Yup, nice. I wonder if you can golf mk_preimage_equiv_lift using the image one...

Mathlib/SetTheory/Cardinal/Basic.lean

b-mehta · 2024-12-16T00:23:47Z

bors d+

mathlib-bors · 2024-12-16T00:23:49Z

✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

vihdzp · 2025-01-05T04:03:28Z

bors r+

…#18933)

mathlib-bors · 2025-01-05T06:18:36Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (133 commits) chore(1000): remove nonexistent fields (#20493) chore(CategoryTheory/Adjunction.Basic, CategoryTheory/Equivalence): change definition of `Adjunction.comp` and `Equivalence.trans` (#20490) feat(Asymptotics): add `Asymptotics.*.*Prod` lemmas (#20458) feat: a conditional kernel is almost everywhere a probability measure (#20430) feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304) feat: `Ico`, `Ioc`, and `Ioo` are not closed or compact (#20479) chore: drop redundant hypothesis in `Module.Dual.eq_of_preReflection_mapsTo` (#20492) feat(FaaDiBruno): derive `DecidableEq` (#20482) chore(SetTheory/Ordinal/Basic): `{x // x < y}` → `Iio y` (#20413) chore: generalize `FormalMultilinearSeries.ofScalars_norm` to `Seminormed` (#20351) chore(MvPolynomial/Localization): golf using TensorProduct (#20309) chore(Combinatorics/Enumerative/Partition): auto-derive DecidableEq (#20277) chore(CategoryTheory): make relevant parameters explicit in `Arrow.homMk`. (#20259) feat: add `IsStarNormal (↑x⁻¹ : R)` instance for `x : Rˣ` (#20091) fix: Stop cancelling builds of master (#20435) chore: update Mathlib dependencies 2025-01-05 (#20485) feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933) chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464) chore: bot validates lean-toolchain on bump/v4.X.0 branches (#20478) feat: shorthand lemmas for the L1 norm (#20383) chore: remove unnecessary adaptation notes (#20467) chore(Algebra/Category/MonCat/Colimits): remove smallness condition (#20473) chore(SetTheory/Ordinal/Arithmetic): `IsLeftCancelAdd Ordinal` (#19888) feat(Algebra): more on `OrthogonalIdempotents` (#18195) feat(Radical): `(radical a).natDegree ≤ a.natDegree` (#20468) feat(Polynomial): `(a^n)' = 0` iff `a' = 0` when `n` doesn't divide the characteristic (#20190) feat(Algebra/Lie): add Lie's theorem (#13480) chore(RingTheory/Generators): make algebra instance a def (#14265) feat(Topology/Group): Lemmas about profinite group (#20282) feat: the empty set is a topological basis iff the space is empty (#20441) chore: make uniqueness of conditionally complete linearly ordered archimedean fields independent of the construction of `Real` (#20242) chore: `inherit_doc`s for notations (#20376) chore: split AEEqOfIntegral into two files, one for each integral type (#20405) chore: split Kernel/MeasurableIntegral (#20427) feat(MeasureTheory/Group/Measure): add ContinuousMulEquiv.isHaarMeasure_map (#20469) fix(Mathlib.Tactic.CC.Datatypes): `cc` raises panic (#20422) feat(Probability/Moments): add lemmas about moment generating functions (#19886) feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCommGroupWithTop (#18954) chore: bump toolchain to v4.15.0 (#20461) chore: update Mathlib dependencies 2025-01-04 (#20463) fix: make `Prod` projection delaborators respond to options, add option to disable (#20455) chore(Algebra): Improve attribute generation (#20451) feat(Polynomial): `(C a * p).degree = p.degree` if `a * p.leadingCoeff ≠ 0` (#20446) feat: add `ENNReal.finStronglyMeasurable_of_measurable` (#20404) doc(Algebra/Lie/Weights/Basic): fix typo (#20450) chore(1000): remove `identifiers` (#20445) feat: add sumPiEquivProdPi and piUnique (#20195) feat: add fst_compProd_apply (#20429) chore: use unsigned measures for Lebesgue decomposition (#20400) feat: Two lemmas on divisibility and coprimality of `expand` (#20143) ...

* origin/master: (189 commits) chore(Algebra): make more names consistent (#20449) feat: Polynomial FLT (#18882) feat: A disjoint union is finite iff all sets are finite, and all but finitely many are empty (#20457) fix: linkfix in 100.yaml (#20517) feat(1000): fill in more entries (#20470) feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `snd` (#16769) feat(ContinuousMultilinearMap): add lemmas about `.prod` (#20462) feat(RingTheory): classification of etale algebras over fields (#20324) fix: Allow multiple builds on staging branch (#20515) feat(CategoryTheory/Shift/Adjunction): properties of `Adjunction.CommShift` (#20337) chore(Data/Multiset/Basic): move the `sub`, `union`, `inter` sections lower (#19863) chore(Topology/UniformSpace/Completion): make coe' argument implicit (#20514) refactor(Algebra/Category/Grp/Colimits): change the construction of colimits in `AddCommGrp` (#20474) feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems (#16544) chore(RingTheory/Finiteness): rename Module.Finite.out (#20506) refactor(CategoryTheory/Limits/Preserves/Ulift): simplify the proof that the universe lifting functor for types preserves all colimits (#20508) feat(CategoryTheory): products in the category of Ind-objects (#20507) chore: remove >9 month old deprecations (#20505) chore(FieldTheory/Galois): small cleanup (#20217) chore(LinearIndependent): generalize to semirings (#20480) chore(NumberTheory/NumberField/AdeleRing): refactor adele rings (#20500) chore: replace `aesop` with `simp` where possible (#20483) chore(1000): remove nonexistent fields (#20493) chore(CategoryTheory/Adjunction.Basic, CategoryTheory/Equivalence): change definition of `Adjunction.comp` and `Equivalence.trans` (#20490) feat(Asymptotics): add `Asymptotics.*.*Prod` lemmas (#20458) feat: a conditional kernel is almost everywhere a probability measure (#20430) feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304) feat: `Ico`, `Ioc`, and `Ioo` are not closed or compact (#20479) chore: drop redundant hypothesis in `Module.Dual.eq_of_preReflection_mapsTo` (#20492) feat(FaaDiBruno): derive `DecidableEq` (#20482) chore(SetTheory/Ordinal/Basic): `{x // x < y}` → `Iio y` (#20413) chore: generalize `FormalMultilinearSeries.ofScalars_norm` to `Seminormed` (#20351) chore(MvPolynomial/Localization): golf using TensorProduct (#20309) chore(Combinatorics/Enumerative/Partition): auto-derive DecidableEq (#20277) chore(CategoryTheory): make relevant parameters explicit in `Arrow.homMk`. (#20259) feat: add `IsStarNormal (↑x⁻¹ : R)` instance for `x : Rˣ` (#20091) fix: Stop cancelling builds of master (#20435) chore: update Mathlib dependencies 2025-01-05 (#20485) feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933) chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464) chore: bot validates lean-toolchain on bump/v4.X.0 branches (#20478) feat: shorthand lemmas for the L1 norm (#20383) chore: remove unnecessary adaptation notes (#20467) chore(Algebra/Category/MonCat/Colimits): remove smallness condition (#20473) chore(SetTheory/Ordinal/Arithmetic): `IsLeftCancelAdd Ordinal` (#19888) feat(Algebra): more on `OrthogonalIdempotents` (#18195) feat(Radical): `(radical a).natDegree ≤ a.natDegree` (#20468) feat(Polynomial): `(a^n)' = 0` iff `a' = 0` when `n` doesn't divide the characteristic (#20190) feat(Algebra/Lie): add Lie's theorem (#13480) chore(RingTheory/Generators): make algebra instance a def (#14265) ...

add lemmas

7f67c4e

vihdzp added the t-set-theory Set theory label Nov 12, 2024

vihdzp mentioned this pull request Nov 12, 2024

[Merged by Bors] - feat(Data/Set): add result that shows a set is even iff it splits into two sets of equal cardinality #18878

Closed

1 task

fix typo

deec5b7

urkud reviewed Nov 14, 2024

View reviewed changes

Mathlib/SetTheory/Cardinal/Basic.lean Outdated Show resolved Hide resolved

vihdzp added 2 commits November 20, 2024 17:43

Merge branch 'master' into vi.card_lems

f5e8abe

generalize thm

ae29233

vihdzp requested a review from b-mehta December 15, 2024 23:18

b-mehta reviewed Dec 15, 2024

View reviewed changes

b-mehta added the awaiting-author A reviewer has asked the author a question or requested changes label Dec 15, 2024

vihdzp added 3 commits December 15, 2024 17:33

Merge branch 'master' into vi.card_lems

3ac1715

add image lems

45e16a4

extend length

894c9e7

leanprover-community-mathlib4-bot added delegated and removed awaiting-author A reviewer has asked the author a question or requested changes labels Dec 16, 2024

mathlib-bors bot pushed a commit that referenced this pull request Jan 5, 2025

feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (…

3c12551

…#18933)

mathlib-bors bot changed the title ~~feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas~~ [Merged by Bors] - feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas Jan 5, 2025

mathlib-bors bot closed this Jan 5, 2025

mathlib-bors bot deleted the vi.card_lems branch January 5, 2025 06:18

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas #18933

[Merged by Bors] - feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas #18933

vihdzp commented Nov 12, 2024

github-actions bot commented Nov 12, 2024 •

edited

Loading

Declarations diff

b-mehta Dec 15, 2024

vihdzp Dec 15, 2024

b-mehta Dec 16, 2024

b-mehta commented Dec 16, 2024

mathlib-bors bot commented Dec 16, 2024

vihdzp commented Jan 5, 2025

mathlib-bors bot commented Jan 5, 2025

		theorem mk_preimage_equiv_lift {β : Type v} (f : α ≃ β) (s : Set β) :
		lift.{v} #(f ⁻¹' s) = lift.{u} #s := by

[Merged by Bors] - feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas #18933

[Merged by Bors] - feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas #18933

Conversation

vihdzp commented Nov 12, 2024

github-actions bot commented Nov 12, 2024 • edited Loading

PR summary 894c9e7d0b

Import changes for modified files

Declarations diff

b-mehta Dec 15, 2024

Choose a reason for hiding this comment

vihdzp Dec 15, 2024

Choose a reason for hiding this comment

b-mehta Dec 16, 2024

Choose a reason for hiding this comment

b-mehta commented Dec 16, 2024

mathlib-bors bot commented Dec 16, 2024

vihdzp commented Jan 5, 2025

mathlib-bors bot commented Jan 5, 2025

github-actions bot commented Nov 12, 2024 •

edited

Loading