infinite_pigeonhole_card_lt — Mathlib

English

If f : β → α and #α < #β with α infinite, then there exists a ∈ α with |α| < |f⁻¹({a})|.

Русский

Если f : β → α и |α| < |β| с α бесконечно, то существует a ∈ α такое, что |α| < |f⁻¹({a})|.

LaTeX

$$$\exists a \in α,\#α < #(f^{-1}\\{a\\}).$$$

Lean4

/-- A function whose codomain's cardinality is infinite but strictly smaller than its domain's
has a fiber with cardinality strictly great than the codomain. -/
theorem infinite_pigeonhole_card_lt {β α : Type u} (f : β → α) (w : #α < #β) (w' : ℵ₀ ≤ #α) :
    ∃ a : α, #α < #(f ⁻¹' { a }) := by
  simp_rw [← succ_le_iff]
  exact
    infinite_pigeonhole_card f (succ #α) (succ_le_of_lt w) (w'.trans (lt_succ _).le)
      ((lt_succ _).trans_le (isRegular_succ w').2.ge)

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