Commit 2024-09-16 10:17 dfad2993

View on Github →

refactor(SetTheory/Cardinal/Ordinal): make Cardinal.aleph' an order iso (#16220) We deprecate alephIdx.initialSeg, alephIdx, alephIdx.relIso, Aleph'.relIso, and aleph'Equiv, which were just stating this idea in slightly different ways. We also make Cardinal.aleph an order embedding.

Estimated changes

modified def Cardinal.aleph'
added theorem Cardinal.aleph'_max
modified theorem Cardinal.aleph'_succ
modified theorem Cardinal.aleph'_zero
modified def Cardinal.aleph
added theorem Cardinal.aleph_max
modified theorem Cardinal.aleph_succ
modified theorem Cardinal.aleph_zero
modified theorem Cardinal.max_aleph_eq