Theorems · Definition · measure theory

StieltjesFunction.measure

{R : Type u_2} →
  [inst : LinearOrder R] →
    [inst_1 : TopologicalSpace R] →
      StieltjesFunction R →
        [OrderTopology R] →
          [CompactIccSpace R] →
            [inst_4 : MeasurableSpace R] →
              [BorelSpace R] → [SecondCountableTopology R] → [DenselyOrdered R] → MeasureTheory.Measure R

The measure associated to a Stieltjes function, giving mass f b - f a to the interval (a, b]. If there is a bot element, it gives zero mass to it.

Defined in

Mathlib.MeasureTheory.Measure.Stieltjes

Cited by

48 results in Mathlib

Foundations

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

Assumes

LinearOrderTopologicalSpaceOrderTopologyCompactIccSpaceMeasurableSpaceBorelSpaceSecondCountableTopologyDenselyOrdered