Mathlib.Data.Fintype.Pigeonhole

Module docstring

{"# Pigeonhole principles in finite types

Main declarations

We provide the following versions of the pigeonholes principle. * Fintype.exists_ne_map_eq_of_card_lt and isEmpty_of_card_lt: Finitely many pigeons and pigeonholes. Weak formulation. * Finite.exists_ne_map_eq_of_infinite: Infinitely many pigeons in finitely many pigeonholes. Weak formulation. * Finite.exists_infinite_fiber: Infinitely many pigeons in finitely many pigeonholes. Strong formulation.

Some more pigeonhole-like statements can be found in Data.Fintype.CardEmbedding. "}

Fintype.exists_ne_map_eq_of_card_lt theorem

(f : α → β) (h : Fintype.card β < Fintype.card α) : ∃ x y, x ≠ y ∧ f x = f y

Full source

/-- The pigeonhole principle for finitely many pigeons and pigeonholes.
This is the `Fintype` version of `Finset.exists_ne_map_eq_of_card_lt_of_maps_to`.
-/
theorem exists_ne_map_eq_of_card_lt (f : α → β) (h : Fintype.card β < Fintype.card α) :
    ∃ x y, x ≠ y ∧ f x = f y :=
  let ⟨x, _, y, _, h⟩ := Finset.exists_ne_map_eq_of_card_lt_of_maps_to h fun x _ => mem_univ (f x)
  ⟨x, y, h⟩

Pigeonhole Principle for Finite Types: Weak Formulation

Informal description

Let $\alpha$ and $\beta$ be finite types, and let $f : \alpha \to \beta$ be a function. If the cardinality of $\beta$ is strictly less than the cardinality of $\alpha$, then there exist distinct elements $x, y \in \alpha$ such that $f(x) = f(y)$.

Function.Embedding.isEmpty_of_card_lt theorem

[Fintype α] [Fintype β] (h : Fintype.card β < Fintype.card α) : IsEmpty (α ↪ β)

Full source

/-- If `‖β‖ < ‖α‖` there are no embeddings `α ↪ β`.
This is a formulation of the pigeonhole principle.

Note this cannot be an instance as it needs `h`. -/
@[simp]
theorem isEmpty_of_card_lt [Fintype α] [Fintype β] (h : Fintype.card β < Fintype.card α) :
    IsEmpty (α ↪ β) :=
  ⟨fun f =>
    let ⟨_x, _y, ne, feq⟩ := Fintype.exists_ne_map_eq_of_card_lt f h
    ne <| f.injective feq⟩

Nonexistence of Injective Functions Between Finite Types with Strictly Smaller Codomain Cardinality

Informal description

Let $\alpha$ and $\beta$ be finite types. If the cardinality of $\beta$ is strictly less than the cardinality of $\alpha$, then there are no injective functions from $\alpha$ to $\beta$.

Finite.exists_ne_map_eq_of_infinite theorem

{α β} [Infinite α] [Finite β] (f : α → β) : ∃ x y : α, x ≠ y ∧ f x = f y

Full source

/-- The pigeonhole principle for infinitely many pigeons in finitely many pigeonholes. If there are
infinitely many pigeons in finitely many pigeonholes, then there are at least two pigeons in the
same pigeonhole.

See also: `Fintype.exists_ne_map_eq_of_card_lt`, `Finite.exists_infinite_fiber`.
-/
theorem Finite.exists_ne_map_eq_of_infinite {α β} [Infinite α] [Finite β] (f : α → β) :
    ∃ x y : α, x ≠ y ∧ f x = f y := by
  simpa [Injective, and_comm] using not_injective_infinite_finite f

Pigeonhole Principle for Infinite Domain and Finite Codomain

Informal description

Let $\alpha$ be an infinite type and $\beta$ a finite type. For any function $f : \alpha \to \beta$, there exist distinct elements $x, y \in \alpha$ such that $f(x) = f(y)$.

Finite.exists_infinite_fiber theorem

[Infinite α] [Finite β] (f : α → β) : ∃ y : β, Infinite (f ⁻¹' { y })

Full source

/-- The strong pigeonhole principle for infinitely many pigeons in
finitely many pigeonholes.  If there are infinitely many pigeons in
finitely many pigeonholes, then there is a pigeonhole with infinitely
many pigeons.

See also: `Finite.exists_ne_map_eq_of_infinite`
-/
theorem Finite.exists_infinite_fiber [Infinite α] [Finite β] (f : α → β) :
    ∃ y : β, Infinite (f ⁻¹' {y}) := by
  classical
    by_contra! hf
    cases nonempty_fintype β
    haveI := fun y => fintypeOfNotInfinite <| hf y
    let key : Fintype α :=
      { elems := univ.biUnion fun y : β => (f ⁻¹' {y}).toFinset
        complete := by simp }
    exact key.false

Strong Pigeonhole Principle: Infinite fibers in finite codomain

Informal description

Let $\alpha$ be an infinite type and $\beta$ a finite type. For any function $f \colon \alpha \to \beta$, there exists an element $y \in \beta$ such that the preimage $f^{-1}(\{y\})$ is infinite.