Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.sum_finpartition

∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : AddCommMonoid V] [inst_1 : TopologicalSpace V]
  [T2Space V] (μ : MeasureTheory.VectorMeasure X V) {s : Set X} {hs : MeasurableSet s} (P : Finpartition ⟨s, hs⟩),
  ∑ p ∈ P.parts, μ ↑p = μ s

The sum of a vector measure μ on a Finpartition of Subtype MeasurableSet equals μ s.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidTopologicalSpaceT2Space