exists_lt_map_eq_of_forall_mem — Mathlib

English

If α is infinite and for all a, f(a) ∈ t, and t is finite, then there exist a,b with a < b and f(a) = f(b).

Русский

Пусть α бесконечно, и для всех a выполняется f(a) ∈ t, где t конечно. Тогда существуют a < b с f(a) = f(b).

LaTeX

$$$[Infinite\ α] \big(\forall a\, f(a) \in t\big) \rightarrow\exists a,b\ (a < b \wedge f(a)=f(b)).$$$

Lean4

theorem exists_lt_map_eq_of_forall_mem [Infinite α] (hf : ∀ a, f a ∈ t) (ht : t.Finite) : ∃ a b, a < b ∧ f a = f b :=
  by
  rw [← mapsTo_univ_iff] at hf
  obtain ⟨a, -, b, -, h⟩ := infinite_univ.exists_lt_map_eq_of_mapsTo hf ht
  exact ⟨a, b, h⟩

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