Theorems · Theorem · measure theory

MeasureTheory.Measure.eqOn_Icc_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},
  a ≠ b →
    ∀ {f g : X → Y},
      f =ᵐ[μ.restrict (Set.Icc a b)] g →
        ContinuousOn f (Set.Icc a b) → ContinuousOn g (Set.Icc a b) → Set.EqOn f g (Set.Icc a b)

Defined in

Mathlib.MeasureTheory.Measure.OpenPos

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderTopologyTopologicalSpaceT2SpaceMeasureTheory.Measure.IsOpenPosMeasureDenselyOrdered