feat(SetTheory/ZFC/Ordinal): von Neumann hierarchy of sets

[vihdzp]

---

• [x] depends on: #16996
• [ ] depends on: #17016
• [x] depends on: #17026
• [ ] depends on: #18239

[github-actions[bot]]

PR summary bf5a0712be

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.SetTheory.ZFC.Neumann (new file)	664

---

Declarations diff

+ exists_mem_vonNeumann + iUnion_vonNeumann + instance : PartialOrder ZFSet + instance : Preorder PSet + isTransitive_vonNeumann + mem_range_self + mem_vonNeumann + rank_vonNeumann + subset_vonNeumann + vonNeumann + vonNeumann_inj + vonNeumann_injective + vonNeumann_mem_vonNeumann_iff + vonNeumann_of_isSuccPrelimit + vonNeumann_strictMono + vonNeumann_subset_vonNeumann_iff + vonNeumann_succ + vonNeumann_zero ++ le_def ++ not_mem_of_subset ++ not_subset_of_mem ++-- le_succ_rank_sUnion ++-- rank_insert ++-- rank_pair ++-- rank_powerset ++-- rank_sUnion_le ++-- rank_singleton

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]

If we're going to talk about cardinalities of the von Neumann hierarchy, it might be nice to first define a preBeth function (analogous to preAleph and preOmega) defined as the beth function but starting from 0. Then #(V_ o) = preBeth o. I'll do this in a separate PR, and the rest should be smooth sailing.

[alreadydone]

I've formalized your suggested proof of #ZFSet=univ here, but it increases transitive imports from 531 to 640 due to Cardinal.Arithmetic. Would you include it in this PR? And can you confirm whether you'll rename the file?

[vihdzp]

I think it'd be best to instead have a Card file collecting at least the #(V_ o) = preBeth o and #ZFSet = univ results.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#16996~~
• ~~leanprover-community/mathlib4#17016~~
• ~~leanprover-community/mathlib4#17026~~
• ~~leanprover-community/mathlib4#18239~~
• ~~leanprover-community/mathlib4#19946~~
• ~~leanprover-community/mathlib4#19967~~ By Dependent Issues (🤖). Happy coding!

[vihdzp]

Moved to #26543