Theorems · Theorem · measure theory

MeasureTheory.Measure.toSignedMeasure_sub_apply

∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ]
  [inst_1 : MeasureTheory.IsFiniteMeasure ν] {i : Set α},
  MeasurableSet i → (μ.toSignedMeasure - ν.toSignedMeasure) i = μ.real i - ν.real i

Defined in

Mathlib.MeasureTheory.VectorMeasure.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure