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.

theorem Fintype.exists_ne_map_eq_of_card_lt {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α → β) (h : card β < card α) : ∃ (x : α) (y : α), x ≠ y ∧ f x = f y

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.

@[simp]

theorem Function.Embedding.isEmpty_of_card_lt {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (h : Fintype.card β < Fintype.card α) : IsEmpty (α ↪ β)

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

Note this cannot be an instance as it needs h.

theorem Finite.exists_ne_map_eq_of_infinite {α : Sort u_4} {β : Sort u_5} [Infinite α] [Finite β] (f : α → β) : ∃ (x : α) (y : α), x ≠ y ∧ f x = f y

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_infinite_fiber {α : Type u_1} {β : Type u_2} [Infinite α] [Finite β] (f : α → β) : ∃ (y : β), Infinite ↑(f ⁻¹' {y})

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