Commit 2025-11-26 18:08 95f10948

View on Github →

feat(SetTheory/ZFC/Ordinal): Lean ordinals to ZFC ordinals (#26544) We define Ordinal.toZFSet and prove that its outputs are precisely the ZFC ordinals. Moved from #19985.

Estimated changes

added theorem ZFSet.insert_eq
added theorem Ordinal.coe_toZFSet
added theorem Ordinal.mem_toPSet_iff
added theorem Ordinal.mk_toPSet
added theorem Ordinal.rank_toPSet
added theorem Ordinal.rank_toZFSet
added theorem Ordinal.toZFSet_succ
added theorem Ordinal.toZFSet_zero
added theorem Ordinal.type_toPSet
added theorem ZFSet.isOrdinal_succ
added theorem PSet.mem_def
added theorem ZFSet.rank_mk