Theorems · Theorem · general topology

exists_monotone_Icc_subset_open_cover_Icc

∀ {ι : Sort u_1} {a b : ℝ},
  a ≤ b →
    ∀ {c : ι → Set ↑(Set.Icc a b)},
      (∀ (i : ι), IsOpen (c i)) →
        Set.univ ⊆ ⋃ i, c i →
          ∃ t, ↑(t 0) = a ∧ Monotone t ∧ (∃ m, ∀ n ≥ m, ↑(t n) = b) ∧ ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ c i

Any open cover c of a closed interval [a, b] in ℝ can be refined to a finite partition into subintervals.

Defined in

Mathlib.Topology.UnitInterval

Cited by

1 results in Mathlib

Foundations

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