English
Given a measurable f: β → α and a target set s with a distinguished point y0 ∈ s, one can construct a sequence of simple functions F_n: β → α with values in s that converge to f pointwise (on a suitable domain), beginning with F_0 ≡ y0.
Русский
Пусть имеем измеримую функцию f: β → α и набор s с помеченной точкой y0 ∈ s; существует последовательность простых функций F_n: β → α со значениями в s, такая что F_n сходится к f по точкам (на соответствующем домене), и F_0 ≡ y0.
LaTeX
$$$\\exists (F_n)_{n∈\\mathbb{N}},\\; F_n: β \\to α\\text{ простая функция},\\; \\forall x, \\; F_n(x) \\in s\\; \\text{и}\\; F_0(x)=y_0;\\; F_n(x) \\to f(x).$$$
Lean4
/-- Approximate a measurable function by a sequence of simple functions `F n` such that
`F n x ∈ s`. -/
noncomputable def approxOn (f : β → α) (hf : Measurable f) (s : Set α) (y₀ : α) (h₀ : y₀ ∈ s) [SeparableSpace s]
(n : ℕ) : β →ₛ α :=
haveI : Nonempty s := ⟨⟨y₀, h₀⟩⟩
comp (nearestPt (fun k => Nat.casesOn k y₀ ((↑) ∘ denseSeq s) : ℕ → α) n) f hf
