Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.ext_iff

∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v w : MeasureTheory.VectorMeasure α M), v = w ↔ ∀ (i : Set α), MeasurableSet i → v i = w i

Defined in

Mathlib.MeasureTheory.VectorMeasure.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidTopologicalSpace