Extra lemmas about unions of intervals

This file contains lemmas about finite unions of intervals which can't be included with the lemmas concerning infinite unions in Mathlib.Order.Interval.Set.Disjoint because we use Finset.range.

theorem Ioc_subset_biUnion_Ioc {X : Type u_1} [LinearOrder X] (N : ℕ) (a : ℕ → X) : Set.Ioc (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Set.Ioc (a i) (a (i + 1))

Union of consecutive intervals contains the interval defined by the initial and final points.

theorem Ico_subset_biUnion_Ico {X : Type u_1} [LinearOrder X] (N : ℕ) (a : ℕ → X) : Set.Ico (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Set.Ico (a i) (a (i + 1))

Union of consecutive intervals contains the interval defined by the initial and final points.