New contributor: #27934 (Order/Interval)

Stream: mathlib4

[Jasper Mulder-Sohn]

Hi all! :wave:

I've been working on the Carleson project the past time, and now the time has come to upstream more of our work.
Just now I opened my first Mathlib PR #27934, which contains a few lemmas about Intervals. I hope to have understood all the guidelines etc. correctly, I have read and tried to follow them.
The PR still needs the carleson label, is that something I can/should do or someone else?

If anything is not up to par, please let me know.

Additionally, there are two more lemmas not yet in the PR:

theorem iUnion_Ico_eq_Ici {f : ℕ → α} (hf : ∀ n, f 0 ≤ f n) (h2f : ¬BddAbove (range f)) :
    ⋃ (i : Nat), Ico (f i) (f (i+1)) = Ici (f 0) := by
  sorry

theorem iUnion_Ioc_eq_Ioi {f : ℕ → α} (hf : ∀ n, f 0 ≤ f n) (h2f : ¬BddAbove (range f)) :
    ⋃ (i : Nat), Ioc (f i) (f (i+1)) = Ioi (f 0) := by
  sorry

I was not sure what their natural home would be or if they should still be generalized. Together with the pairwise disjointness results they partition Ioi (f 0), which was what was needed for Carleson.

Your feedback and suggestions are welcome. Thanks in advance for your time!

[Aaron Liu]

I needed something similar recently, and I found docs#Monotone.biUnion_Ico_Ioc_map_succ

[Eric Wieser]

I guess monotonicity isn't needed here

[Jasper Mulder-Sohn]

Oh, I see that the pairwise disjoint statements already exist, they are in that file. Thanks for that pointer! I will update the PR.
For the iUnion statements, note that I am not assuming monotonicity and this is on purpose.

[Jasper Mulder-Sohn]

By analogy, but without assuming monotonicity, I now arrived at:

variable {α β : Type*} [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] [LinearOrder β]

theorem biUnion_Ici_Ico_map_succ {f : α → β} {a : α} (hf : ∀ i ∈ Ici a, f a ≤ f i)
    (h2f : ¬BddAbove (f '' Ici a)) :
    ⋃ i ∈ Ici a, Ico (f i) (f (succ i)) = Ici (f a) := by
  sorry

What would be a natural home for this? Seeing as it is not assuming monotonicity anymore.
Do we want a simplified statement for the typical case Nat and 0?

[Jasper Mulder-Sohn]

I have created another PR #27966 for this result and a similar one for Ioc.
I have added the results to the existing PR #27934 because they depend on that.