Theorems · Theorem · measure theory

MeasureTheory.OuterMeasure.ofFunction_eq

∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} (s : Set α),
  (∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t) →
    (∀ (s : ℕ → Set α), m (⋃ i, s i) ≤ ∑' (i : ℕ), m (s i)) → (MeasureTheory.OuterMeasure.ofFunction m m_empty) s = m s

Defined in

Mathlib.MeasureTheory.OuterMeasure.OfFunction

Cited by

3 results in Mathlib

Foundations

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