Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.variation_smul

∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : NormedAddCommGroup V]
  {μ : MeasureTheory.VectorMeasure X V} {𝕜 : Type u_3} [inst_1 : NormedField 𝕜] [inst_2 : NormedSpace 𝕜 V] {c : 𝕜},
  (c • μ).variation = ‖c‖₊ • μ.variation

Defined in

Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedFieldNormedSpace