English
Under hypotheses, the union over i ≥ a of Ioc intervals maps to the open interval Ioi at f a.
Русский
При гипотезах объединение по i ≥ a интервалов Ioc отображается в открытый интервал Ioi в точке f a.
LaTeX
$$\displaystyle \bigcup_{i \ge a} Ioc(f(i), f(\operatorname{succ} i)) = Ioi(f(a))$$
Lean4
/-- If `α` is a linear archimedean succ order and `β` is a linear order, then for any monotone
function `f` and `m n : α`, the union of intervals `Set.Ioc (f i) (f (Order.succ i))`, `m ≤ i < n`,
is equal to `Set.Ioc (f m) (f n)` -/
theorem biUnion_Ico_Ioc_map_succ [SuccOrder α] [IsSuccArchimedean α] [LinearOrder β] {f : α → β} (hf : Monotone f)
(m n : α) : ⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n) :=
by
rcases le_total n m with hnm | hmn
· rw [Ico_eq_empty_of_le hnm, Ioc_eq_empty_of_le (hf hnm), biUnion_empty]
· refine Succ.rec ?_ ?_ hmn
· simp only [Ioc_self, Ico_self, biUnion_empty]
· intro k hmk ihk
rw [← Ioc_union_Ioc_eq_Ioc (hf hmk) (hf <| le_succ _), union_comm, ← ihk]
by_cases hk : IsMax k
· rw [hk.succ_eq, Ioc_self, empty_union]
· rw [Ico_succ_right_eq_insert_of_not_isMax hmk hk, biUnion_insert]
