Def Ordinal.isInitialIso

Modification history

2024-10-16 11:05
Mathlib/SetTheory/Cardinal/Aleph.lean
feat(SetTheory/Cardinal/Aleph): define initial ordinals (#16964)
Added Ordinal.isInitialIsoView on Github →