Theorems · Theorem · measure theory

MeasureTheory.OuterMeasure.ofFunction_union_of_top_of_nonempty_inter

∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} {s t : Set α},
  (∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤) →
    (MeasureTheory.OuterMeasure.ofFunction m m_empty) (s ∪ t) =
      (MeasureTheory.OuterMeasure.ofFunction m m_empty) s + (MeasureTheory.OuterMeasure.ofFunction m m_empty) t

If m u = ∞ for any set u that has nonempty intersection both with s and t, then μ (s ∪ t) = μ s + μ t, where μ = MeasureTheory.OuterMeasure.ofFunction m m_empty. E.g., if α is an (e)metric space and m u = ∞ on any set of diameter ≥ r, then this lemma implies that μ (s ∪ t) = μ s + μ t on any two sets such that r ≤ edist x y for all x ∈ s and y ∈ t.

Defined in

Mathlib.MeasureTheory.OuterMeasure.OfFunction

Cited by

2 results in Mathlib

Foundations

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