Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.exists_variation_le_add

∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] (μ : MeasureTheory.VectorMeasure X V) {s : Set X},
  MeasurableSet s →
    ∀ {ε : NNReal},
      0 < ε →
        μ.variation s ≠ ⊤ →
          ∃ P,
            (∀ t ∈ P, t ⊆ s) ∧
              (↑P).PairwiseDisjoint id ∧ (∀ t ∈ P, MeasurableSet t) ∧ μ.variation s ≤ ∑ p ∈ P, ‖μ p‖ₑ + ↑ε

Measure version of preVariation.exists_Finpartition_sum_ge.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceENormedAddCommMonoidT2Space