Theorem ENat.card_pos

Modification history

2026-07-09 14:40
Mathlib/SetTheory/Cardinal/Finite.lean
feat(MeasureTheory): mass of `count.real` (#40367) …
Modified ENat.card_posView on Github →
2025-09-23 05:58
Mathlib/SetTheory/Cardinal/Finite.lean
feat(Data/Set/Card): every finset of card less than `ENat.card α` doesn't contain some element (#29900) …
Added ENat.card_posView on Github →