Theorems · Theorem · measure theory

measurable_limit_of_tendsto_metrizable_ae

∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : MeasurableSpace β] [BorelSpace β] {ι : Type u_3} [Nonempty ι]
  {μ : MeasureTheory.Measure α} {f : ι → α → β} {L : Filter ι} [L.IsCountablyGenerated],
  (∀ (n : ι), AEMeasurable (f n) μ) →
    (∀ᵐ (x : α) ∂μ, ∃ l, Filter.Tendsto (fun n => f n x) L (nhds l)) →
      ∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) L (nhds (f_lim x))

Defined in

Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Cited by

1 results in Mathlib

Foundations

Depth 184 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceTopologicalSpaceTopologicalSpace.PseudoMetrizableSpaceMeasurableSpaceBorelSpaceNonemptyFilter.IsCountablyGenerated