Theorem ENat.card_pos_iff_nonempty

Modification history

2026-02-23 18:16

Mathlib/SetTheory/Cardinal/Finite.lean

feat(SetTheory/Cardinal): more lemmas about `ENat` (#33909) …

Added ENat.card_pos_iff_nonempty View on Github →