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.