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.lean 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.