Theorems · Theorem · order theory

Ioc_subset_biUnion_Ioc

∀ {X : Type u_1} [inst : 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.

Defined in

Mathlib.Order.Interval.Set.Union

Cited by

1 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrder