Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.iSup_sum_finpartition_parts

∀ {X : Type u_1} {mX : MeasurableSpace X} (μ : MeasureTheory.VectorMeasure X ENNReal) {s : Set X}
  (hs : MeasurableSet s), ⨆ P, ∑ p ∈ P.parts, μ ↑p = μ s

For μ : VectorMeasure X ℝ≥0∞ and measurable s, the supremum over Finpartitions of ⟨s, hs⟩ : Subtype MeasurableSet of the sum of μ over parts equals μ s.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Cited by

1 results in Mathlib

Foundations

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