Theorems · Theorem · measure theory

MeasureTheory.Measure.eq_of_ae_eq

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {m : MeasurableSpace X} [inst_1 : TopologicalSpace Y]
  [T2Space Y] {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {f g : X → Y},
  f =ᵐ[μ] g → Continuous f → Continuous g → f = g

If two continuous functions are a.e. equal, then they are equal.

Defined in

Mathlib.MeasureTheory.Measure.OpenPos

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceT2SpaceMeasureTheory.Measure.IsOpenPosMeasure