Theorems · Theorem · measure theory

MeasureTheory.Measure.sub_apply

∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsFiniteMeasure ν],
  MeasurableSet s → ν ≤ μ → (μ - ν) s = μ s - ν s

This application lemma only works in special circumstances. Given knowledge of when μ ≤ ν and ν ≤ μ, a more general application lemma can be written.

Defined in

Mathlib.MeasureTheory.Measure.Sub

Cited by

5 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasure