Theorems · Theorem · measure theory

MeasureTheory.OuterMeasure.ofFunction_eq_iInf_mem

∀ {α : Type u_1} (m : Set α → ENNReal) (m_empty : m ∅ = 0) {P : Set α → Prop},
  (∀ (s : Set α), ¬P s → m s = ⊤) →
    ∀ (s : Set α),
      (MeasureTheory.OuterMeasure.ofFunction m m_empty) s =
        ⨅ t, ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i)

ofFunction of a set s is the infimum of ∑ᵢ, m (tᵢ) for all collections of sets tᵢ that cover s, with all tᵢ satisfying a predicate P such that m is infinite for sets that don't satisfy P. This is similar to ofFunction_apply, except that the sets tᵢ satisfy P. The hypothesis m_top applies in particular to a function of the form extend m'.

Defined in

Mathlib.MeasureTheory.OuterMeasure.OfFunction

Cited by

2 results in Mathlib

Foundations

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