Theorems · Theorem · measure theory

MeasureTheory.AddContent.inducedOuterMeasure_eq

∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C),
  m.IsSigmaSubadditive → s ∈ C → (MeasureTheory.inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯) s = m s

For m : AddContent C sigma-sub-additive, finite on C, the inducedOuterMeasure given by m coincides with m on C.

Defined in

Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Cited by

1 results in Mathlib

Foundations

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