Theorem Cardinal.lt_omega_iff_card_lt

Modification history

2024-12-16 00:26

Mathlib/SetTheory/Cardinal/Aleph.lean

feat(SetTheory/Cardinal/Arithmetic): cardinality of ordinal exponential (#17813) …

Added Cardinal.lt_omega_iff_card_lt View on Github →