exists_infinite_fiber — Mathlib

English

A function whose codomain is infinite but strictly smaller than its domain has an infinite fiber: there exists a ∈ α such that f⁻¹({a}) is infinite.

Русский

Функция, чья кодомножество бесконечно, но строго меньше домена, имеет бесконечное волокно: существует a ∈ α такое, что f⁻¹({a}) бесконечно.

LaTeX

$$$\exists a:\, α,\ Infinite( f^{-1}\\{a\\} ).$$$

Lean4

/-- A function whose codomain's cardinality is infinite but strictly smaller than its domain's
has an infinite fiber. -/
theorem exists_infinite_fiber {β α : Type u} (f : β → α) (w : #α < #β) (w' : Infinite α) :
    ∃ a : α, Infinite (f ⁻¹' { a }) := by
  simp_rw [Cardinal.infinite_iff] at w' ⊢
  obtain ⟨a, ha⟩ := infinite_pigeonhole_card_lt f w w'
  exact ⟨a, w'.trans ha.le⟩

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