Theorems · Theorem · general topology

MeasureTheory.measurableSet_tendsto_fun

∀ {ι : Type u_2} {γ : Type u_3} {β : Type u_5} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] [Countable ι]
  {l : Filter ι} [l.IsCountablyGenerated] [inst_4 : TopologicalSpace γ] [SecondCountableTopology γ]
  [TopologicalSpace.PseudoMetrizableSpace γ] [OpensMeasurableSpace γ] {f : ι → β → γ},
  (∀ (i : ι), Measurable (f i)) →
    ∀ {g : β → γ}, Measurable g → MeasurableSet {x | Filter.Tendsto (fun n => f n x) l (nhds (g x))}

The set of points for which a sequence of measurable functions converges to a given function is measurable.

Defined in

Mathlib.MeasureTheory.Constructions.Polish.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceCountableFilter.IsCountablyGeneratedTopologicalSpaceSecondCountableTopologyTopologicalSpace.PseudoMetrizableSpaceOpensMeasurableSpace