Theorems · Theorem · measure theory

MeasureTheory.Measure.ext_of_Ioc

∀ {α : Type u_5} [inst : TopologicalSpace α] {_m : MeasurableSpace α} [SecondCountableTopology α]
  [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [BorelSpace α] [NoMinOrder α]
  (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ],
  (∀ ⦃a b : α⦄, a < b → μ (Set.Ioc a b) = ν (Set.Ioc a b)) → μ = ν

Two measures which are finite on closed-open intervals are equal if they agree on all open-closed intervals.

Defined in

Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceSecondCountableTopologyConditionallyCompleteLinearOrderOrderTopologyBorelSpaceNoMinOrderMeasureTheory.IsLocallyFiniteMeasure