infinite pigeonhole

Stream: Is there code for X?

[Scott Morrison]

I would like the following infinite pigeonhole principle:

import set_theory.cofinality

example {α β : Type*} (w : cardinal.mk β < cardinal.mk α) (w' : cardinal.omega ≤ cardinal.mk β)
  (f : α → β) : ∃ b : β, set.infinite (f ⁻¹' {b}) :=
sorry

The only infinite pigeonhole principle I see in set_theory.cofinality (e.g. src#ordinal.infinite_pigeonhole) is ... more complicated! Is there an easy way to get this from that?

[Floris van Doorn]

import set_theory.cofinality

open cardinal
lemma foo {α β : Type*} (w : mk β < mk α) (w' : omega ≤ mk β)
  (f : α → β) : ∃ b : β, mk β < mk (f ⁻¹' {b}) :=
begin
  simp_rw [← succ_le],
  exact ordinal.infinite_pigeonhole_card f
    ((mk β).succ)
    (succ_le.mpr w)
    (w'.trans (lt_succ_self _).le)
    ((lt_succ_self _).trans_le (succ_is_regular w').2.ge),
end

example {α β : Type*} (w : cardinal.mk β < cardinal.mk α) (w' : cardinal.omega ≤ cardinal.mk β)
  (f : α → β) : ∃ b : β, set.infinite (f ⁻¹' {b}) :=
begin
  simp_rw [← set.infinite_coe_iff, cardinal.infinite_iff],
  cases foo w w' f with b hb,
  exact ⟨b, w'.trans hb.le⟩,
end

The first lemma should probably be in mathlib.

[Floris van Doorn]

The idea is to use docs#ordinal.infinite_pigeonhole_card (which is more general) and then take for θ any regular cardinal between #β and #α. In this case we can take (#β).succ.

[Scott Morrison]

Thanks @Floris, I understand now! These are useful.