English
The infimum over a family m of outer measures equals the bounded by infimum of sInfGen: sInf m = OuterMeasure.boundedBy (sInfGen m).
Русский
Инфинум семейства внешних мер равенboundedBy (sInfGen m).
LaTeX
$$$ sInf\\, m = \\mathrm{boundedBy}(sInfGen\\, m)$$$
Lean4
/-- 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. -/
theorem sInf_apply {m : Set (OuterMeasure α)} {s : Set α} (h : m.Nonempty) :
sInf m s = ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' n, ⨅ (μ : OuterMeasure α) (_ : μ ∈ m), μ (t n) := by
simp_rw [sInf_eq_boundedBy_sInfGen, boundedBy_apply, iSup_sInfGen_nonempty h]
