tendsto_approx — Mathlib

English

StronglyMeasurable f has a witness sequence of simple functions converging pointwise to f.

Русский

Sильная измеримость имеет последовательность простых функций, сходящуюся к f по каждой точке.

LaTeX

$$$\\forall x, Tendsto (n\\mapsto hf.approx n x)\\\\to f(x)$$$

Lean4

protected theorem tendsto_approx {_ : MeasurableSpace α} (hf : StronglyMeasurable f) :
    ∀ x, Tendsto (fun n => hf.approx n x) atTop (𝓝 (f x)) :=
  hf.choose_spec

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