measurable_of_tendsto_metrizable — Mathlib

English

If f_i are measurable and converge to g in a metrizable space, then g is measurable.

Русский

Если f_i измеримы и сходятся к g в метризуемом пространстве, то g измеримо.

LaTeX

$$$\\forall i,\\ Measurable(f_i) \\land Tendsto f_i u (\\mathcal{NH} g) \\Rightarrow Measurable(g)$$$

Lean4

/-- A sequential limit of measurable functions valued in a (pseudo) metrizable space is
measurable. -/
theorem measurable_of_tendsto_metrizable {f : ℕ → α → β} {g : α → β} (hf : ∀ i, Measurable (f i))
    (lim : Tendsto f atTop (𝓝 g)) : Measurable g :=
  measurable_of_tendsto_metrizable' atTop hf lim

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