Theorems · Theorem · measure theory

MeasureTheory.StronglyMeasurable.limUnder

∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace E] [Countable ι]
  {l : Filter ι} [l.IsCountablyGenerated] {f : ι → X → E} [hE : Nonempty E]
  [TopologicalSpace.IsCompletelyMetrizableSpace E],
  (∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) →
    MeasureTheory.StronglyMeasurable fun x => l.limUnder fun x_1 => f x_1 x

Defined in

Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceCountableFilter.IsCountablyGeneratedNonemptyTopologicalSpace.IsCompletelyMetrizableSpace