Theorems · Theorem · measure theory

aemeasurable_of_tendsto_metrizable_ae

∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : MeasurableSpace β] [BorelSpace β] {ι : Type u_3}
  {μ : MeasureTheory.Measure α} {f : ι → α → β} {g : α → β} (u : Filter ι) [hu : u.NeBot] [u.IsCountablyGenerated],
  (∀ (n : ι), AEMeasurable (f n) μ) → (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) u (nhds (g x))) → AEMeasurable g μ

Defined in

Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Cited by

7 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceTopologicalSpace.PseudoMetrizableSpaceMeasurableSpaceBorelSpaceFilter.NeBotFilter.IsCountablyGenerated