Theorems · Definition · measure theory

MeasureTheory.VectorMeasure.restrict

{α : Type u_1} →
  {mα : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommMonoid M] →
        [inst_1 : TopologicalSpace M] → MeasureTheory.VectorMeasure α M → Set α → MeasureTheory.VectorMeasure α M

The restriction of a vector measure on some set.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Basic

Cited by

139 results in Mathlib

Foundations

Depth 67 from the axioms, rests on 1,302 definitions · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidTopologicalSpace