English
The infinite pigeonhole principle: for f : β → α, if β is infinite and α is small in a cofinal sense, then some fiber f⁻¹({a}) has size equal to |β|.
Русский
Неограниченный принцип пиджохола: для f : β → α, если β бесконечно по мощности и α относительно β малого по коф, то существует элемент a ∈ α, для которого мощность прообраза f⁻¹({a}) равна |β|.
LaTeX
$$$\exists a \in \alpha,\ #(f^{-1}\\{a\\}) = #\\beta.$$$
Lean4
/-- The infinite pigeonhole principle -/
theorem infinite_pigeonhole {β α : Type u} (f : β → α) (h₁ : ℵ₀ ≤ #β) (h₂ : #α < (#β).ord.cof) :
∃ a : α, #(f ⁻¹' { a }) = #β :=
by
have : ∃ a, #β ≤ #(f ⁻¹' { a }) := by
by_contra! h
apply mk_univ.not_lt
rw [← preimage_univ, ← iUnion_of_singleton, preimage_iUnion]
exact
mk_iUnion_le_sum_mk.trans_lt
((sum_le_iSup _).trans_lt <| mul_lt_of_lt h₁ (h₂.trans_le <| cof_ord_le _) (iSup_lt h₂ h))
obtain ⟨x, h⟩ := this
refine ⟨x, h.antisymm' ?_⟩
rw [le_mk_iff_exists_set]
exact ⟨_, rfl⟩
