English
If δ ≥ 0, then addNSMul h δ is a monotone function of its index.
Русский
Если δ ≥ 0, то функция addNSMul h δ по индексу монотонна.
LaTeX
$$Monotone (Set.Icc.addNSMul h δ)$$
Lean4
/-- Any open cover `c` of a closed interval `[a, b]` in ℝ
can be refined to a finite partition into subintervals. -/
theorem exists_monotone_Icc_subset_open_cover_Icc {ι} {a b : ℝ} (h : a ≤ b) {c : ι → Set (Icc a b)}
(hc₁ : ∀ i, IsOpen (c i)) (hc₂ : univ ⊆ ⋃ i, c i) :
∃ t : ℕ → Icc a b, t 0 = a ∧ Monotone t ∧ (∃ m, ∀ n ≥ m, t n = b) ∧ ∀ n, ∃ i, Icc (t n) (t (n + 1)) ⊆ c i :=
by
obtain ⟨δ, δ_pos, ball_subset⟩ := lebesgue_number_lemma_of_metric isCompact_univ hc₁ hc₂
have hδ := half_pos δ_pos
refine ⟨addNSMul h (δ / 2), addNSMul_zero h, monotone_addNSMul h hδ.le, addNSMul_eq_right h hδ, fun n ↦ ?_⟩
obtain ⟨i, hsub⟩ := ball_subset (addNSMul h (δ / 2) n) trivial
exact ⟨i, fun t ht ↦ hsub ((abs_sub_addNSMul_le h hδ.le n ht).trans_lt <| half_lt_self δ_pos)⟩
