Theorems · Theorem · combinatorics
Finset.exists_ne_map_eq_of_card_lt_of_maps_to
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β},
t.card < s.card → ∀ {f : α → β}, Set.MapsTo f ↑s ↑t → ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f yIf there are more pigeons than pigeonholes, then there are two pigeons in the same pigeonhole.
See also Set.exists_ne_map_eq_of_encard_lt_of_maps_to and
Set.exists_ne_map_eq_of_ncard_lt_of_maps_to.
- Defined in
- Mathlib.Data.Finset.Card
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- SetLike.coestatement and proof · cited by 8,199
- Finset.cardstatement and proof · cited by 2,327
- Set.MapsTostatement and proof · cited by 732
- LT.lt.not_geproof · cited by 305
- Finset.card_le_card_of_injOnproof · cited by 16
Cited by5
Results whose statement or proof uses this declaration.
- Fintype.exists_ne_map_eq_of_card_ltproof · cited by 7
- Real.exists_int_int_abs_mul_sub_leproof · cited by 2
- Finset.exists_ne_map_eq_of_card_image_ltproof · cited by 2
- Int.Matrix.exists_ne_zero_int_vec_norm_leproof · cited by 1
- SimpleGraph.IsTuranMaximal.card_partsproof · cited by 1