Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.restrict_eq_self

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

Defined in

Mathlib.MeasureTheory.VectorMeasure.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommMonoidTopologicalSpace