Theorems · Definition · measure theory

MeasureTheory.VectorMeasure.ennrealVariation

{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.VectorMeasure X ENNReal

The variation of a VectorMeasure as an ℝ≥0∞-valued VectorMeasure.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Variation.Defs

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceENormedAddCommMonoidT2Space