Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.restrict_restrict

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

Defined in

Mathlib.MeasureTheory.VectorMeasure.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommMonoidTopologicalSpace