Theorems · Theorem · measure theory

MeasureTheory.SignedMeasure.singularPart_add

∀ {α : Type u_1} {m : MeasurableSpace α} (s t : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α)
  [s.HaveLebesgueDecomposition μ] [t.HaveLebesgueDecomposition μ],
  (s + t).singularPart μ = s.singularPart μ + t.singularPart μ

Defined in

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SignedMeasure.HaveLebesgueDecompositionMeasureTheory.SignedMeasure.HaveLebesgueDecomposition