Theorem ENat.card_lt_top

Modification history

2026-10-28 01:55
Mathlib/SetTheory/Cardinal/Finite.lean
feat(SetTheory/Cardinal/Finite): simp lemmas for `[E]Nat.card` (#44408) …
Modified ENat.card_lt_topView on Github →
2025-11-02 19:19
Mathlib/SetTheory/Cardinal/Finite.lean
feat(Set): finite cardinality iff `[Finite]` (#30245) …
Added ENat.card_lt_topView on Github →