exists_lt_map_eq_of_mapsTo — Mathlib

English

If s is infinite and f maps s into t with MapsTo, and t is finite, then there exist x,y ∈ s with x < y and f(x) = f(y).

Русский

Если s бесконечно, f отображает s в t посредством MapsTo, и t конечно, тогда существуют x,y ∈ s такие, что x < y и f(x) = f(y).

LaTeX

$$$\exists x \in s, \exists y \in s, x < y \land f(x) = f(y).$$$

Lean4

theorem exists_lt_map_eq_of_mapsTo (hs : s.Infinite) (hf : MapsTo f s t) (ht : t.Finite) :
    ∃ x ∈ s, ∃ y ∈ s, x < y ∧ f x = f y :=
  let ⟨x, hx, y, hy, hxy, hf⟩ := hs.exists_ne_map_eq_of_mapsTo hf ht
  hxy.lt_or_gt.elim (fun hxy => ⟨x, hx, y, hy, hxy, hf⟩) fun hyx => ⟨y, hy, x, hx, hyx, hf.symm⟩

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