English
If t.encard < s.encard and MapsTo f s t, then there exist a1, a2 in s with a1 ≠ a2 and f a1 = f a2.
Русский
Если t.encard < s.encard и MapsTo f s t, то существуют a1, a2 в s такие, что a1 ≠ a2 и f a1 = f a2.
LaTeX
$$$\\exists a_1 \\in s, \\exists a_2 \\in s, a_1 \\neq a_2 \\land f a_1 = f a_2$$$
Lean4
/-- A version of the pigeonhole principle for `Set`s rather than `Finset`s.
See also `Finset.exists_ne_map_eq_of_card_lt_of_maps_to` and
`Set.exists_ne_map_eq_of_ncard_lt_of_maps_to`. -/
theorem exists_ne_map_eq_of_encard_lt_of_maps_to (hc : t.encard < s.encard) (hf : MapsTo f s t) :
∃ᵉ (a₁ ∈ s) (a₂ ∈ s), a₁ ≠ a₂ ∧ f a₁ = f a₂ := by
contrapose! hc
suffices Function.Injective (hf.restrict f)
by
let f' : s ↪ t := ⟨hf.restrict, this⟩
exact f'.encard_le
simpa only [hf.restrict_inj, not_imp_not] using hc
