Theorem Set.exists_subset_ncard_eq

Modification history

2026-11-10 14:11
Mathlib/Data/Set/Card.lean
feat(Data/Set/Card): `ncard` of `image2`, and sets of a given `ncard` (#45617) …
Added Set.exists_subset_ncard_eqView on Github →