Theorem Set.one_lt_ncard_of_nonempty_of_even

Modification history

2024-09-11 15:57
Mathlib/Data/Set/Card.lean
feat(Data/Set/Finite): added lemmas about cardinality of finite sets (#15652) …
Added Set.one_lt_ncard_of_nonempty_of_evenView on Github →