aemeasurable_of_tendsto_metrizable_ae'

English

A limit (AE) of measurable functions valued in a metrizable space is AEMeasurable.

Русский

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

LaTeX

$$$aemeasurable\_of\_tendsto\_metrizable\_ae'\\, (f, g)$$$

Lean4

theorem aemeasurable_of_tendsto_metrizable_ae' {μ : Measure α} {f : ℕ → α → β} {g : α → β}
    (hf : ∀ n, AEMeasurable (f n) μ) (h_ae_tendsto : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))) :
    AEMeasurable g μ :=
  aemeasurable_of_tendsto_metrizable_ae atTop hf h_ae_tendsto

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