[Merged by Bors] - feat(SetTheory/ZFC): add `ZFSet.card` by staroperator · Pull Request #29365 · leanprover-community/mathlib4

staroperator · 2025-09-05T12:02:00Z

The same as ZFSet.rank, we define ZFSet.card as ZFSet.{u} → Cardinal.{u} and prove some basic properties.

depends on: [Merged by Bors] - feat(SetTheory/ZFC): add ZFSet.iUnion #30841
depends on: [Merged by Bors] - refactor(SetTheory/ZFC): deduplicate coercion to sets #31287

github-actions · 2025-09-05T12:03:15Z

PR summary 16e4c581cf

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ card
+ card_empty
+ card_image_le
+ card_insert
+ card_insert_le
+ card_mono
+ card_pair_of_ne
+ card_powerset
+ card_singleton
+ card_union_le
+ cardinalMk_coe_sort
+ iSup_card_le_card_iUnion
+ iSup_mk_le_mk_iUnion
+ inter_eq_left_of_subset
+ inter_eq_right_of_subset
+ lift_card_iUnion_le_sum_card
+ lift_card_range_le
+ powersetEquiv

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).

vihdzp

Thank you for this! This was a long-standing TODO on my personal list.

Speaking of that, one of the results I wanted to prove was that (V_ o).card = preBeth o. I think you should have all the tools to prove that - if it's not too hard, could you add it to the PR?

staroperator · 2025-09-06T13:59:45Z

Thank you for this! This was a long-standing TODO on my personal list.

Speaking of that, one of the results I wanted to prove was that (V_ o).card = preBeth o. I think you should have all the tools to prove that - if it's not too hard, could you add it to the PR?

I have! But that proof is not trivial and will depend on #26544. I will make a draft PR for that later

YaelDillies

Thanks for the PR! Here's a first batch of comments

YaelDillies · 2025-10-04T09:49:49Z

Mathlib/SetTheory/Cardinal/Basic.lean

+theorem iSup_mk_le_mk_iUnion {α : Type u} {ι : Type v} {f : ι → Set α} :
+    ⨆ i, #(f i) ≤ #(⋃ i, f i) :=
+  ciSup_le' fun _ => mk_le_mk_of_subset (subset_iUnion _ _)


Are you sure we really need this lemma? I think we should instead make sure that simp can prove it

I don't think simp can prove an inequality. It is definitely used in #29393, and since we already have Cardinal.mk_iUnion_le_sum_mk that gives an upper bound for #(⋃ i, f i), it should be natural to have a lower bound for it.

I don't think simp can prove an inequality

Have you seen iSup_le_iff ?

Have you seen iSup_le_iff ?

Now I know, thanks to point it out 😃 But still, I don't think simp can help in this lemma.

Mathlib/SetTheory/ZFC/Basic.lean

Mathlib/SetTheory/ZFC/Cardinal.lean

Mathlib/SetTheory/ZFC/Basic.lean

mathlib4-merge-conflict-bot · 2025-11-04T13:27:50Z

This pull request has conflicts, please merge master and resolve them.

Mathlib/SetTheory/ZFC/Basic.lean

Mathlib/SetTheory/Cardinal/Basic.lean

YaelDillies · 2025-11-04T20:06:37Z

Mathlib/SetTheory/ZFC/Cardinal.lean

+def card (x : ZFSet.{u}) : Cardinal.{u} := #(Shrink x.toSet)
+
+/-- `ZFSet.card x` is equal to the cardinality of `x` as a set of `ZFSet`s. -/
+theorem card_eq {x : ZFSet.{u}} : lift.{u + 1, u} (card x) = #x.toSet := by


I would turn this around and call it mk_toSet

Looks good. Should that also be @[simp]?

Probably yes

Probably not, because it will make simp non-confluent on card (x ∪ y).toSet and others

Do you mind expanding?

I mean this makes simp on #(x ∪ y).toSet produce different normal forms based on choice of order of rewriting lemmas. card_toSet will rewrite it to lift (card (x ∪ y)) while toSet_union (which is already simp) will rewrite it to #(x.toSet ∪ y.toSet), both can not be rewritten further.

(Sorry, the card above should be Cardinal.mk.)

Do you mean #(x ∪ y).toSet?

Also, since # is Cardinal.mk should we call it mk_toSet? Or cardinalMk_toSet?

But yes, good point

Or cardinal_toSet? That has a few precedents like LinearIndependent.cardinal_le_rank.

Mathlib/SetTheory/ZFC/Cardinal.lean

Mathlib/SetTheory/ZFC/Basic.lean

mathlib4-merge-conflict-bot · 2025-11-19T08:00:23Z

This pull request has conflicts, please merge master and resolve them.

mathlib4-dependent-issues-bot · 2025-11-21T12:26:39Z

This PR/issue depends on:

~~[Merged by Bors] - feat(SetTheory/ZFC): add ZFSet.iUnion #30841~~
~~[Merged by Bors] - refactor(SetTheory/ZFC): deduplicate coercion to sets #31287~~
By Dependent Issues (🤖). Happy coding!

YaelDillies

Thanks!

maintainer delegate

Mathlib/SetTheory/ZFC/Cardinal.lean

github-actions · 2025-11-22T16:15:31Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

Co-authored-by: Yaël Yanis Dillies <yael.dillies@gmail.com>

Mathlib/SetTheory/ZFC/Cardinal.lean

b-mehta

Thanks!

bors merge

The same as `ZFSet.rank`, we define `ZFSet.card` as `ZFSet.{u} → Cardinal.{u}` and prove some basic properties. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

mathlib-bors · 2025-11-23T06:30:03Z

Pull request successfully merged into master.

Build succeeded:

…lib4 * 'master' of https://github.com/leanprover-community/mathlib4: (3130 commits) feat(SetTheory/ZFC): add `ZFSet.card` (leanprover-community#29365) feat: grind annotations for `choose_spec` (leanprover-community#31927) chore(scripts): update nolints.json (leanprover-community#31975) feat(Analysis): cos (n * π) = (-1) ^ n (leanprover-community#31971) chore: rename `mul_le_mul_right'` to `mul_le_mul_left` (leanprover-community#30242) chore: update Mathlib dependencies 2025-11-22 (leanprover-community#31955) feat(MeasureTheory): ae-measurability notation wrt non-standard sigma-algebra (leanprover-community#31910) doc: add missing spaces around doc code blocks (leanprover-community#31917) chore: update Mathlib dependencies 2025-11-22 (leanprover-community#31945) chore: shortcut instance for `Nat` to be mul-torsion-free (leanprover-community#31027) doc(Topology/Algebra/Algebra): outdated TODO (leanprover-community#31944) feat(EqHaar): add `addHaar_nnreal_smul` (leanprover-community#31922) chore(Algebra): make invertibleInv an instance (leanprover-community#31916) chore(Algebra): change two statements in CubicDiscriminant (leanprover-community#31912) chore(MeasureTheory): mark `map_dirac` as simp (leanprover-community#31909) feat: `LinearOrder` instance for `Empty` (leanprover-community#31889) chore: deprecate all remaining modules in `Analysis/NormedSpace` (leanprover-community#31913) feat(SimpleGraph): weaker condition for paths in acyclic graphs (leanprover-community#25814) chore: do not set `group` when declaring option (leanprover-community#31888) chore: clean up more unused `Decidable*` instances in types (leanprover-community#31934) ...

github-actions bot added the t-set-theory Set theory label Sep 5, 2025

vihdzp approved these changes Sep 6, 2025

View reviewed changes

staroperator mentioned this pull request Sep 7, 2025

[Merged by Bors] - feat(SetTheory/ZFC): card (V_ o) = preBeth o #29393

Closed

3 tasks

leanprover-community-bot-assistant assigned YaelDillies Sep 30, 2025

YaelDillies reviewed Oct 4, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 4, 2025

staroperator added 5 commits October 4, 2025 11:01

add

784f314

format

8275d40

rename

98b32be

update Mathlib.lean

79dc951

apply suggestions

8bebe30

staroperator force-pushed the zfset_card branch from 0d4ee83 to 8bebe30 Compare October 4, 2025 15:01

staroperator removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 4, 2025

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 24, 2025

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 4, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 4, 2025

staroperator added 2 commits November 4, 2025 14:55

Merge branch 'master' into zfset_card

1071ecd

update

b37e444

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 4, 2025

YaelDillies reviewed Nov 4, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 4, 2025

staroperator added 2 commits November 4, 2025 18:45

golf

64b586b

add powersetEquiv

46b7259

staroperator commented Nov 5, 2025

View reviewed changes

Mathlib/SetTheory/ZFC/Basic.lean Show resolved Hide resolved

reorder

de34774

staroperator added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Nov 5, 2025

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Nov 5, 2025

staroperator and others added 3 commits November 5, 2025 08:19

implicit

1204abc

unsimp

e4246e1

golf

efee422

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 5, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 21, 2025

staroperator added 3 commits November 22, 2025 10:31

Merge branch 'master' into zfset_card

4d8c5cc

update

9150cc9

Merge remote-tracking branch 'origin/zfset_card' into zfset_card

bc8045c

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 22, 2025

YaelDillies approved these changes Nov 22, 2025

View reviewed changes

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

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

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Nov 22, 2025

Apply suggestions from code review

201f0db

Co-authored-by: Yaël Yanis Dillies <yael.dillies@gmail.com>

YaelDillies reviewed Nov 22, 2025

View reviewed changes

Mathlib/SetTheory/ZFC/Cardinal.lean Show resolved Hide resolved

empty line

1b4cdec

b-mehta reviewed Nov 23, 2025

View reviewed changes

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Nov 23, 2025

mathlib-bors bot changed the title ~~feat(SetTheory/ZFC): add ZFSet.card~~ [Merged by Bors] - feat(SetTheory/ZFC): add ZFSet.card Nov 23, 2025

mathlib-bors bot closed this Nov 23, 2025

Conversation

staroperator commented Sep 5, 2025 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Sep 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 16e4c581cf

Import changes for modified files

Declarations diff

Uh oh!

vihdzp left a comment

Choose a reason for hiding this comment

Uh oh!

staroperator commented Sep 6, 2025

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib4-merge-conflict-bot commented Nov 4, 2025

Uh oh!

Uh oh!

Uh oh!

YaelDillies Nov 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

staroperator Nov 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

staroperator Nov 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Nov 21, 2025

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Nov 22, 2025

Uh oh!

Uh oh!

b-mehta left a comment

Choose a reason for hiding this comment

staroperator commented Sep 5, 2025 •

edited by YaelDillies

Loading

github-actions bot commented Sep 5, 2025 •

edited

Loading

YaelDillies Nov 4, 2025 •

edited

Loading

staroperator Nov 5, 2025 •

edited

Loading

staroperator Nov 5, 2025 •

edited

Loading