Theorems · Definition · measure theory

MeasureTheory.preVariation

{X : Type u_1} →
  [inst : MeasurableSpace X] →
    (f : Set X → ENNReal) → MeasureTheory.IsSigmaSubadditiveSetFun f → f ∅ = 0 → MeasureTheory.Measure X

The Measure X built from a σ-subadditive function.

Defined in: Mathlib.MeasureTheory.Measure.PreVariation
Cited by: 5 results in Mathlib
Foundations: Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement · cited by 10,939
ENNRealstatement and proof · cited by 9,879
MeasureTheory.VectorMeasure.ennrealToMeasureproof · cited by 13
MeasureTheory.ennrealPreVariationproof · cited by 10
MeasureTheory.IsSigmaSubadditiveSetFunstatement and proof · cited by 7

Cited by6

Results whose statement or proof uses this declaration.

MeasureTheory.VectorMeasure.variationproof · cited by 125
MeasureTheory.VectorMeasure.variation_negproof · cited by 3
MeasureTheory.preVariation.congr_simpstatement and proof · cited by 2
MeasureTheory.preVariation_zerostatement · cited by 1
MeasureTheory.VectorMeasure.variation_applystatement · cited by 0
MeasureTheory.preVariation_applystatement · cited by 0