exists_ne_map_eq_of_infinite — Mathlib

English

There exists y ∈ β such that the fiber f^{-1}({y}) is infinite when α is infinite and β is finite.

Русский

Существет y ∈ β такое, что f^{-1}({y}) бесконечно, если α бесконечно и β конечно.

LaTeX

$$$\\exists y: \\beta, Infinite\\left(f^{-1}({y})\\right).$$$

Lean4

/-- The pigeonhole principle for infinitely many pigeons in finitely many pigeonholes. If there are
infinitely many pigeons in finitely many pigeonholes, then there are at least two pigeons in the
same pigeonhole.

See also: `Fintype.exists_ne_map_eq_of_card_lt`, `Finite.exists_infinite_fiber`.
-/
theorem exists_ne_map_eq_of_infinite {α β} [Infinite α] [Finite β] (f : α → β) : ∃ x y : α, x ≠ y ∧ f x = f y := by
  simpa [Injective, and_comm] using not_injective_infinite_finite f

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