Theorem Set.one_le_ncard_insert

Modification history

2025-11-04 20:26
Mathlib/Data/Set/Card.lean
feat(Set): helper lemmas about set cardinality (#29833) …
Added Set.one_le_ncard_insertView on Github →