Theorems · Theorem · measure theory

MeasureTheory.Measure.eqOn_open_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] {U : Set X} {f g : X → Y},
  f =ᵐ[μ.restrict U] g → IsOpen U → ContinuousOn f U → ContinuousOn g U → Set.EqOn f g U

If two functions are a.e. equal on an open set and are continuous on this set, then they are equal on this set.

Defined in

Mathlib.MeasureTheory.Measure.OpenPos

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceT2SpaceMeasureTheory.Measure.IsOpenPosMeasure