Theorems · Theorem · measure theory

MeasureTheory.Measure.eqOn_Ico_of_ae_eq

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X]
  {m : MeasurableSpace X} [inst_3 : TopologicalSpace Y] [T2Space Y] (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure]
  [DenselyOrdered X] {a b : X} {f g : X → Y},
  f =ᵐ[μ.restrict (Set.Ico a b)] g →
    ContinuousOn f (Set.Ico a b) → ContinuousOn g (Set.Ico a b) → Set.EqOn f g (Set.Ico a b)

Defined in

Mathlib.MeasureTheory.Measure.OpenPos

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderTopologyTopologicalSpaceT2SpaceMeasureTheory.Measure.IsOpenPosMeasureDenselyOrdered