approxOn_range_nonneg — Mathlib

English

If α has a zero and is ordered, and f(x)≥0 for all x, then the approximants F_n(x) are nonnegative and lie in range f ∪ {0}.

Русский

Пусть α имеет нуль и упорядочено; если f(x)≥0, тогда F_n(x) неотрицательны и принадлежат диапазону range f ∪ {0}.

LaTeX

$$$0 \\le f \\quad\\Rightarrow\\quad 0 \\le approxOn\\; f\\; h_f\\; (range f \\cup \\{0\\})\\; 0\\; (by\\ simp)\\; n.$$$

Lean4

theorem approxOn_range_nonneg [Zero α] [Preorder α] {f : β → α} (hf : 0 ≤ f) {hfm : Measurable f}
    [SeparableSpace (range f ∪ {0} : Set α)] (n : ℕ) : 0 ≤ approxOn f hfm (range f ∪ {0}) 0 (by simp) n :=
  by
  have : range f ∪ {0} ⊆ Set.Ici 0 :=
    by
    simp only [Set.union_singleton, Set.insert_subset_iff, Set.mem_Ici, le_refl, true_and]
    rintro - ⟨x, rfl⟩
    exact hf x
  exact fun _ ↦ this <| approxOn_mem ..

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