Theorem Set.ncard_image2_le

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.ncard_image2_leView on Github →