Pigeonhole principle

[urkud]

Formalize pigeonhole principles

• for finsets;
• for fintypes;
• for measure_spaces: PR'd in [Merged by Bors] - feat(measure_theory/measure_space): pigeonhole principle in a measure space #2538 ;
• for ordinals: already here in set_theory/cofinality but needs a proper docstring (I failed to understand the (mk β).ord.cof trick).

All these principles easily follow from existing lemmas. I have some of them locally, will PR soon.

[kckennylau]

is the statement for fintype essentially that if \a \to \b is injective then card \a \le card \b?

[urkud]

@kckennylau Yes, and we already have this for finsets. But I'd like to have these wrappers:

variables {α : Type*} {β : Type*} [fintype α] [fintype β] (f : α → β)
example (h : card β < card α) : ∃ x y (h : x ≠ y), f x = f y := sorry
example (n : nat) (hn : n * card β < card α) : ∃ y : β, n < card (f ⁻¹' {y}) := sorry

[jalex-stark]

@kckennylau Yes, and we already have this for finsets. But I'd like to have these wrappers:

variables {α : Type*} {β : Type*} [fintype α] [fintype β] (f : α → β)
example (h : card β < card α) : ∃ x y (h : x ≠ y), f x = f y := sorry
example (n : nat) (hn : n * card β < card α) : ∃ y : β, n < card (f ⁻¹' {y}) := sorry

like this? the sorry is supposed to be filled by pigeonhole for finset. where does that live?

example (h : card β < card α) : ∃ x y (h : x ≠ y), f x = f y := 
begin
  set x := elems α,
  set y := elems β,
  have key : ∃ a a' ∈ x, a ≠ a' ∧ f a = f a' := sorry,
  rcases key with ⟨ a, a', _, _, h1, h2⟩,
  use [a, a'], split; assumption,
end