Theorems · Theorem · measure theory

MeasureTheory.tendstoInMeasure_ae_unique

∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : EMetricSpace E] {g h : α → E} {f : ι → α → E} {u : Filter ι} [u.NeBot] [u.IsCountablyGenerated],
  MeasureTheory.TendstoInMeasure μ f u g → MeasureTheory.TendstoInMeasure μ f u h → g =ᵐ[μ] h

The limit in measure is ae unique.

Defined in

Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Cited by

0 results in Mathlib

Foundations

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

Assumes

EMetricSpaceFilter.NeBotFilter.IsCountablyGenerated