aemeasurable_of_tendsto — Mathlib

English

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

Русский

Предел а.е.-измеримых функций ENNReal по общему фильтру остаётся а.е.-измеримым.

LaTeX

$$$\text{aemeasurable_of_tendsto}'$$$

Lean4

/-- A limit of a.e.-measurable `ℝ≥0∞`-valued functions is a.e.-measurable. -/
theorem aemeasurable_of_tendsto {f : ℕ → α → ℝ≥0∞} {g : α → ℝ≥0∞} {μ : Measure α} (hf : ∀ i, AEMeasurable (f i) μ)
    (hlim : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (g a))) : AEMeasurable g μ :=
  aemeasurable_of_tendsto' atTop hf hlim

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