English
A pigeonhole principle for a cardinal θ below the domain: for f : β → α and θ a cardinal with θ ≤ |β| and θ ≤ aleph0 and α small enough, there exists a ∈ α with θ ≤ #(f⁻¹({a})).
Русский
Пиджохол для кардиналa ниже множества: для f : β → α и θ кардинал с θ ≤ |β| и θ ≤ aleph0 и α будет достаточно мал, существует a ∈ α такой, что θ ≤ #(f⁻¹({a})).
LaTeX
$$$\exists a \in α,\ θ \le |f^{-1}\\{a\\}|.$$$
Lean4
/-- Pigeonhole principle for a cardinality below the cardinality of the domain -/
theorem infinite_pigeonhole_card {β α : Type u} (f : β → α) (θ : Cardinal) (hθ : θ ≤ #β) (h₁ : ℵ₀ ≤ θ)
(h₂ : #α < θ.ord.cof) : ∃ a : α, θ ≤ #(f ⁻¹' { a }) :=
by
rcases le_mk_iff_exists_set.1 hθ with ⟨s, rfl⟩
obtain ⟨a, ha⟩ := infinite_pigeonhole (f ∘ Subtype.val : s → α) h₁ h₂
use a; rw [← ha, @preimage_comp _ _ _ Subtype.val f]
exact mk_preimage_of_injective _ _ Subtype.val_injective
