Theorems · Theorem · measure theory

MeasureTheory.measureReal_inter_add_sdiff

∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet t →
    autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_inter_add_sdiff._auto_1 → μ.real (s ∩ t) + μ.real (s \ t) = μ.real s

Defined in

Mathlib.MeasureTheory.Measure.Real

Cited by

2 results in Mathlib

Foundations

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