English
The half-open interval Ico(a0, aN) is contained in the union of the consecutive half-open intervals Ico(ai, a(i+1)).
Русский
Полуоткрытый интервал Ico(a0, aN) содержится в объединении последовательных полуоткрытых интервалов Ico(ai, a(i+1)).
LaTeX
$$$$ Ico(a_0, a_N) \subseteq \bigcup_{i=0}^{N-1} Ico(a_i, a_{i+1}). $$$$
Lean4
/-- Union of consecutive intervals contains the interval defined by the initial and final points. -/
theorem Ico_subset_biUnion_Ico {X : Type*} [LinearOrder X] (N : ℕ) (a : ℕ → X) :
Ico (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Ico (a i) (a (i + 1)) := by
induction N with
| zero => simp
| succ N ih =>
calc
_ ⊆ Ico (a 0) (a N) ∪ Ico (a N) (a (N + 1)) := Ico_subset_Ico_union_Ico
_ ⊆ _ := by simpa [Finset.range_add_one] using union_subset_union_right (Ico (a N) (a (N + 1))) ih
