Theorems · Theorem · measure theory

MeasureTheory.OuterMeasure.sInf_apply

∀ {α : Type u_1} {m : Set (MeasureTheory.OuterMeasure α)} {s : Set α},
  m.Nonempty → (sInf m) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, μ (t n)

The value of the Infimum of a nonempty set of outer measures on a set is not simply the minimum value of a measure on that set: it is the infimum sum of measures of countable set of sets that covers that set, where a different measure can be used for each set in the cover.

Defined in

Mathlib.MeasureTheory.OuterMeasure.OfFunction

Cited by

3 results in Mathlib

Foundations

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