exists_ne_map_eq_of_card_lt — Mathlib

English

For finite α, β and a function f: α → β, if |β| < |α|, there exist x ≠ y with f(x) = f(y).

Русский

Для конечных множеств α, β и отображения f: α → β, если |β| < |α|, существуют x ≠ y такие что f(x) = f(y).

LaTeX

$$$\\exists x\\exists y\\,(x \\neq y) \\land f(x) = f(y).$$$

Lean4

/-- The pigeonhole principle for finitely many pigeons and pigeonholes.
This is the `Fintype` version of `Finset.exists_ne_map_eq_of_card_lt_of_maps_to`.
-/
theorem exists_ne_map_eq_of_card_lt (f : α → β) (h : Fintype.card β < Fintype.card α) : ∃ x y, x ≠ y ∧ f x = f y :=
  let ⟨x, _, y, _, h⟩ := Finset.exists_ne_map_eq_of_card_lt_of_maps_to h fun x _ => mem_univ (f x)
  ⟨x, y, h⟩

Похожие утверждения