exists_ne_map_eq_of_card_lt_of_maps_to

English

If there are more pigeons than holes, then two pigeons share a hole.

Русский

Если камодонов больше, чем ячейки, то две птицы занимают одну ячейку.

LaTeX

$$If #t < #s then ∃ x,y ∈ s with x ≠ y and f(x) = f(y) where hf: MapsTo f s t$$

Lean4

/-- If 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`. -/
theorem exists_ne_map_eq_of_card_lt_of_maps_to (hc : #t < #s) {f : α → β} (hf : Set.MapsTo f s t) :
    ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y := by
  classical
  by_contra! hz
  refine hc.not_ge (card_le_card_of_injOn f hf ?_)
  intro x hx y hy
  contrapose
  exact hz x hx y hy

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