Theorems · Theorem · measure theory

MeasureTheory.Measure.ext_of_Icc

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

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

Defined in

Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceSecondCountableTopologyLinearOrderOrderTopologyCompactIccSpaceBorelSpaceMeasureTheory.IsLocallyFiniteMeasure