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