Infinite pigeonhole principle

This file proves variants of the infinite pigeonhole principle.

TODO

Generalize universes of results.

theorem Cardinal.infinite_pigeonhole {β α : Type u} (f : β → α) (h₁ : aleph0 ≤ mk β) (h₂ : mk α < (mk β).ord.cof) : ∃ (a : α), mk ↑(f ⁻¹' {a}) = mk β

The infinite pigeonhole principle

theorem Cardinal.infinite_pigeonhole_card {β α : Type u} (f : β → α) (θ : Cardinal.{u}) (hθ : θ ≤ mk β) (h₁ : aleph0 ≤ θ) (h₂ : mk α < θ.ord.cof) : ∃ (a : α), θ ≤ mk ↑(f ⁻¹' {a})

Pigeonhole principle for a cardinality below the cardinality of the domain

theorem Cardinal.infinite_pigeonhole_set {β α : Type u} {s : Set β} (f : ↑s → α) (θ : Cardinal.{u}) (hθ : θ ≤ mk ↑s) (h₁ : aleph0 ≤ θ) (h₂ : mk α < θ.ord.cof) : ∃ (a : α) (t : Set β) (h : t ⊆ s), θ ≤ mk ↑t ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f ⟨x, ⋯⟩ = a

theorem Cardinal.infinite_pigeonhole_card_lt {β α : Type u} (f : β → α) (h : mk α < mk β) (hβ : aleph0 ≤ mk β) : ∃ (a : α), mk α < mk ↑(f ⁻¹' {a})

A function whose domain's cardinality is infinite and strictly greater than its codomain's has a fiber with cardinality strictly great than the codomain.

theorem Cardinal.exists_infinite_fiber {β α : Type u} (f : β → α) (h : mk α < mk β) [Infinite β] : ∃ (a : α), Infinite ↑(f ⁻¹' {a})

A function whose domain's cardinality is infinite and strictly greater than its codomain's has an infinite fiber.

theorem Cardinal.exists_infinite_fiber' {β α : Type u} (f : β → α) (h : mk α < mk β) [Infinite α] : ∃ (a : α), Infinite ↑(f ⁻¹' {a})

A weaker version of exists_infinite_fiber that requires codomain to be infinite.

theorem Cardinal.exists_uncountable_fiber {β α : Type u} (f : β → α) (h : mk α < mk β) [Uncountable β] : ∃ (a : α), Uncountable ↑(f ⁻¹' {a})

A function whose domain's cardinality is uncountable and strictly greater than its codomain's has an uncountable fiber.

theorem Cardinal.le_range_of_union_finset_eq_univ {α : Type u_1} {β : Type u_2} [Infinite β] (f : α → Finset β) (w : ⋃ (a : α), ↑(f a) = Set.univ) : mk β ≤ mk ↑(Set.range f)

If an infinite type β can be expressed as a union of finite sets, then the cardinality of the collection of those finite sets must be at least the cardinality of β.

@[deprecated Cardinal.le_range_of_union_finset_eq_univ (since := "2026-01-17")]

theorem Cardinal.le_range_of_union_finset_eq_top {α : Type u_1} {β : Type u_2} [Infinite β] (f : α → Finset β) (w : ⋃ (a : α), ↑(f a) = Set.univ) : mk β ≤ mk ↑(Set.range f)

Alias of Cardinal.le_range_of_union_finset_eq_univ.

---

If an infinite type β can be expressed as a union of finite sets, then the cardinality of the collection of those finite sets must be at least the cardinality of β.