Theorems · Definition · measure theory

MeasureTheory.VectorMeasure.variation

{X : Type u_1} →
  {mX : MeasurableSpace X} →
    {V : Type u_2} →
      [inst : TopologicalSpace V] →
        [inst_1 : ENormedAddCommMonoid V] → [T2Space V] → MeasureTheory.VectorMeasure X V → MeasureTheory.Measure X

The variation of a VectorMeasure as a Measure.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Variation.Defs

Cited by

125 results in Mathlib

Foundations

Depth 171 from the axioms, rests on 4,732 definitions · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceENormedAddCommMonoidT2Space