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)