measurable_of_tendsto — Mathlib

English

A limit (over a general filter) of measurable ENNReal-valued functions is measurable.

Русский

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

LaTeX

$$$\text{Measurable of Tendsto}'$$$

Lean4

/-- A sequential limit of measurable `ℝ≥0∞`-valued functions is measurable. -/
theorem measurable_of_tendsto {f : ℕ → α → ℝ≥0∞} {g : α → ℝ≥0∞} (hf : ∀ i, Measurable (f i))
    (lim : Tendsto f atTop (𝓝 g)) : Measurable g :=
  measurable_of_tendsto' atTop hf lim

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