Theorems · Theorem · measure theory

MeasureTheory.inducedOuterMeasure_union_of_false_of_nonempty_inter

∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} {s t : Set α},
  (∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → ¬P u) →
    (MeasureTheory.inducedOuterMeasure m P0 m0) (s ∪ t) =
      (MeasureTheory.inducedOuterMeasure m P0 m0) s + (MeasureTheory.inducedOuterMeasure m P0 m0) t

If P u is False for any set u that has nonempty intersection both with s and t, then μ (s ∪ t) = μ s + μ t, where μ = inducedOuterMeasure m P0 m0. E.g., if α is an (e)metric space and P u = diam u < 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.Induced

Cited by

0 results in Mathlib

Foundations

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