Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.exists_lt_sum_of_lt_variation

∀ {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 →
    ∀ {a : ENNReal},
      a < μ.variation s →
        ∃ P, (∀ t ∈ P, t ⊆ s) ∧ (↑P).PairwiseDisjoint id ∧ (∀ t ∈ P, MeasurableSet t) ∧ a < ∑ p ∈ P, ‖μ p‖ₑ

Measure version of preVariation.exists_Finpartition_sum_gt.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceENormedAddCommMonoidT2Space