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 ..