Theorems · Theorem · measure theory

measurableSet_tendsto

∀ {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {x : MeasurableSpace β} [inst : MeasurableSpace γ] [Countable δ]
  {l : Filter δ} [l.IsCountablyGenerated] (l' : Filter γ) [l'.IsCountablyGenerated] [hl' : l'.IsMeasurablyGenerated]
  {f : δ → β → γ}, (∀ (i : δ), Measurable (f i)) → MeasurableSet {x | Filter.Tendsto (fun n => f n x) l l'}

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

Defined in

Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceCountableFilter.IsCountablyGeneratedFilter.IsCountablyGeneratedFilter.IsMeasurablyGenerated