Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.zero_le_restrict_subset

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

Defined in

Mathlib.MeasureTheory.VectorMeasure.Basic

Cited by

8 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddCommMonoidPartialOrder