Theorem Ordinal.not_bddAbove_isInitial

Modification history

2024-10-16 11:05

Mathlib/SetTheory/Cardinal/Aleph.lean

feat(SetTheory/Cardinal/Aleph): define initial ordinals (#16964)

Added Ordinal.not_bddAbove_isInitial View on Github →