English
A set version of the pigeonhole principle: for f : s → α with s a subset of β, if θ ≤ |s| and θ ≥ aleph0 and α < cof(θ), then there exist a ∈ α and t ⊆ s such that θ ≤ |t| and f is constant on t.
Русский
Версия принципа пиджохола для множества: для f : s → α, где s ⊆ β, если θ ≤ |s| и θ бесконечен и α < cof(θ), то найдутся a ∈ α и t ⊆ s такие, что θ ≤ |t| и f постоянно на t.
LaTeX
$$$\exists a \in α,\exists t \subseteq s,\ θ \le |t| \land \forall x\,(x \in t \Rightarrow f(x)=a).$$$
Lean4
theorem infinite_pigeonhole_set {β α : Type u} {s : Set β} (f : s → α) (θ : Cardinal) (hθ : θ ≤ #s) (h₁ : ℵ₀ ≤ θ)
(h₂ : #α < θ.ord.cof) : ∃ (a : α) (t : Set β) (h : t ⊆ s), θ ≤ #t ∧ ∀ ⦃x⦄ (hx : x ∈ t), f ⟨x, h hx⟩ = a :=
by
obtain ⟨a, ha⟩ := infinite_pigeonhole_card f θ hθ h₁ h₂
refine ⟨a, {x | ∃ h, f ⟨x, h⟩ = a}, ?_, ?_, ?_⟩
· rintro x ⟨hx, _⟩
exact hx
· refine ha.trans (ge_of_eq <| Quotient.sound ⟨Equiv.trans ?_ (Equiv.subtypeSubtypeEquivSubtypeExists _ _).symm⟩)
simp only [coe_eq_subtype, mem_singleton_iff, mem_preimage, mem_setOf_eq]
rfl
rintro x ⟨_, hx'⟩; exact hx'
