Theorem Cardinal.toENat_eq_iff_of_le_aleph0

Modification history

2026-02-23 18:16
Mathlib/SetTheory/Cardinal/ENat.lean
feat(SetTheory/Cardinal): more lemmas about `ENat` (#33909) …
Modified Cardinal.toENat_eq_iff_of_le_aleph0View on Github →
2024-12-01 00:08
Mathlib/SetTheory/Cardinal/ENat.lean
feat: introduce ENat.card, and use it in place of PartENat.card (#19624)
Added Cardinal.toENat_eq_iff_of_le_aleph0View on Github →