Theorems · Theorem · measure theory

MeasureTheory.preVariation.sum_le_preVariationFun_of_subset

∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal) {s₁ s₂ : Set X} (hs₁ : MeasurableSet s₁),
  MeasurableSet s₂ → s₁ ⊆ s₂ → ∀ (P : Finpartition ⟨s₁, hs₁⟩), ∑ p ∈ P.parts, f ↑p ≤ MeasureTheory.preVariationFun f s₂

If P is a partition of s₁ and s₁ ⊆ s₂ then ∑ p ∈ P.parts, f p ≤ preVariationFun f s₂.

Defined in

Mathlib.MeasureTheory.Measure.PreVariation

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace