good place for `iUnion_Iic_rat_coe`

Stream: mathlib4

[Moritz Firsching]

I'm cleaning up Probability/Kernel/CondCdf and was wondering what would be a good place for
theorem Real.iUnion_Iic_rat : ⋃ r : ℚ, Iic (r : ℝ) = univ := ...
Any ideas?
or is there perhaps even a more general lemma lurking underneath here?

[Ruben Van de Velde]

Trivially generalizes to

import Mathlib

set_option autoImplicit false

open Set

variable {α : Type*} [LinearOrderedField α] [Archimedean α]
theorem iUnion_Iic_rat : ⋃ r : ℚ, Iic (r : α) = univ := by
  ext1 x
  simp only [mem_iUnion, mem_Iic, mem_univ, iff_true_iff]
  obtain ⟨r, hr⟩ := exists_rat_gt x
  exact ⟨r, hr.le⟩

[Emilie (Shad Amethyst)]

The rationals are dense in the reals, so many permutations of this theorem can be constructed (Iio, Ici, Ioi, etc.)
I wonder if this can't be made generic to dense sets, akin to Dense.biUnion_uniformity_ball

[Yaël Dillies]

Yes, this will be true for any function with cobounded range

[Ruben Van de Velde]

Expecting a fully general proof from Yaël in 3... 2...

[Yaël Dillies]

variable {ι : Sort*} {α : Type*} [LinearOrder α] {f : ι → α}

lemma Set.iUnion_Iic_of_not_bddAbove_range (hf : ¬ BddAbove (range f) :
    ⋃ i, f i = univ := by
  simpa [eq_univ_iff_forall, BddAbove] using hf

(untested)

[Emilie (Shad Amethyst)]

Simp ends up recommending

variable {ι : Sort*} {α : Type*} [LinearOrder α] {f : ι → Set α} in
lemma Set.iUnion_Iic_of_not_bddAbove_range (hf : ¬ BddAbove (range f)) :
    ⋃ i, f i = univ := by
  simp only [OrderTop.bddAbove, not_true_eq_false] at hf

This does work, though:

variable {ι : Sort*} {α : Type*} [LinearOrder α] {f : ι → α} in
lemma Set.iUnion_Iio_of_not_bddAbove_range (hf : ¬ BddAbove (range f)) :
    ⋃ i, Iio (f i) = univ := by
  simpa [not_bddAbove_iff, Set.eq_univ_iff_forall] using hf

[Emilie (Shad Amethyst)]

Wait no hold on

I'm a dummy, Set α has a top element (Set.univ), so f must be bounded above if it maps to Set α

[Emilie (Shad Amethyst)]

I can't seem to do better than this:

variable {ι : Sort*} {α : Type*} [LinearOrder α] {f : ι → α} in
lemma Set.iUnion_Iic_of_not_bddAbove_range (hf : ¬ BddAbove (range f)) :
    ⋃ i, Iic (f i) = univ := by
  rw [← Set.univ_subset_iff]
  apply subset_trans (subset_of_eq (Set.iUnion_Iio_of_not_bddAbove_range hf).symm)
  gcongr
  exact Iio_subset_Iic_self

[Moritz Firsching]

Cool, this is great! The proof also uses the dualized version, which I did like so:

lemma Set.iInter_Iic_of_not_bddBelow_range (hf : ¬ BddBelow (range f)) :
    ⋂ i, Iic (f i) = ∅ := by
  simpa [not_bddBelow_iff, Set.eq_empty_iff_forall_not_mem] using hf

lemma Set.iInter_Iio_of_not_bddBelow_range (hf : ¬ BddBelow (range f)) :
    ⋂ i, Iio (f i) = ∅ := by
  apply eq_empty_of_subset_empty
  rw [← Set.iInter_Iic_of_not_bddBelow_range hf]
  gcongr
  exact Iio_subset_Iic_self

Would it also be useful to have

lemma notBddAbove_coe: ¬(BddAbove <| range (fun (x : ℚ) ↦ (x : ℝ))) := ...

and

lemma notBddBelow_coe: ¬(BddBelow <| range (fun (x : ℚ) ↦ (x : ℝ))) :=...

as separate lemmas somewhere to connect the generalized version to the one actually needed in Probability/Kernel/CondCdf?

Also one question remains:
What would be a good place for those lemmas?

[Moritz Firsching]

Made a pr with the best place I could find: https://github.com/leanprover-community/mathlib4/pull/10298