Theorem Finset.exists_ne_map_eq_of_card_image_lt

Modification history

2025-10-24 09:13
Mathlib/Data/Finset/Card.lean
feat(Data/Finset/Card): add some more Pigeonhole Principle theorems `exists_ne_map_eq_of_card_image_lt` and `not_injOn_of_card_image_lt` (#28077) …
Added Finset.exists_ne_map_eq_of_card_image_ltView on Github →