Commit 2025-07-28 07:12 409dc309

View on Github →

feat(SetTheory/ZFC/VonNeumann): von Neumann hierarchy of sets (#26543) Ported from #17027. For extra discussion on this PR, see Zulip.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean

Modified Mathlib/SetTheory/ZFC/Basic.lean

added theorem ZFSet.mem_range_self

Modified Mathlib/SetTheory/ZFC/Ordinal.lean

Created Mathlib/SetTheory/ZFC/VonNeumann.lean

added theorem ZFSet.exists_mem_vonNeumann

added theorem ZFSet.iUnion_vonNeumann

added theorem ZFSet.isTransitive_vonNeumann

added theorem ZFSet.mem_vonNeumann'

added theorem ZFSet.mem_vonNeumann

added theorem ZFSet.mem_vonNeumann_of_subset

added theorem ZFSet.mem_vonNeumann_succ

added theorem ZFSet.rank_vonNeumann

added theorem ZFSet.subset_vonNeumann

added theorem ZFSet.subset_vonNeumann_self

added theorem ZFSet.vonNeumann_inj

added theorem ZFSet.vonNeumann_injective

added theorem ZFSet.vonNeumann_mem_of_lt

added theorem ZFSet.vonNeumann_mem_vonNeumann_iff

added theorem ZFSet.vonNeumann_of_isSuccPrelimit

added theorem ZFSet.vonNeumann_strictMono

added theorem ZFSet.vonNeumann_subset_of_le

added theorem ZFSet.vonNeumann_subset_vonNeumann_iff

added theorem ZFSet.vonNeumann_succ

added theorem ZFSet.vonNeumann_zero