exists_ne_map_eq_of_mapsTo — Mathlib

English

If s is infinite and f maps s into a finite set t, then there exist x≠y in s with f(x)=f(y).

Русский

Если s бесконечно, а образ f(s) конечен, то существуют различные x,y ∈ s такие, что f(x)=f(y).

LaTeX

$$$ s.Infinite \land (f''s).Finite \Rightarrow \exists x\in s,\exists y\in s, x\neq y \land f x = f y $$$

Lean4

theorem exists_ne_map_eq_of_mapsTo {s : Set α} {t : Set β} {f : α → β} (hs : s.Infinite) (hf : MapsTo f s t)
    (ht : t.Finite) : ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y :=
  by
  contrapose! ht
  exact infinite_of_injOn_mapsTo (fun x hx y hy => not_imp_not.1 (ht x hx y hy)) hf hs

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