exists_monotone_Icc_subset_open_cover_unitInterval

English

Any open cover of the unit interval can be refined to a finite partition into subintervals, analogous to the Icc case.

Русский

Любое открытое покрытие единичного интервала может быть приведено к конечному разбиению на подпериоды, аналогично случаю Icc.

LaTeX

$$Exists (monotone partition) for unitInterval similar to exists_monotone_Icc_subset_open_cover_Icc$$

Lean4

/-- Any open cover of the unit interval can be refined to a finite partition into subintervals. -/
theorem exists_monotone_Icc_subset_open_cover_unitInterval {ι} {c : ι → Set I} (hc₁ : ∀ i, IsOpen (c i))
    (hc₂ : univ ⊆ ⋃ i, c i) :
    ∃ t : ℕ → I, t 0 = 0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ n, ∃ i, Icc (t n) (t (n + 1)) ⊆ c i :=
  by
  simp_rw [← Subtype.coe_inj]
  exact exists_monotone_Icc_subset_open_cover_Icc zero_le_one hc₁ hc₂

Похожие утверждения