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.