English
For any nonempty set m and s, sInf m s equals the infimum over all countable coverings t of s of the sum of inner infima of m over t(n).
Русский
Для любого не пустого множества m и множества s, sInf m s равно инфимууму по покрытиям t: s ⊆ ⋃ t(n) и сумме по n встроенных инфимума м(t(n)).
LaTeX
$$$ sInf m\\, s = \\inf_{t: \\mathbb{N} \\to Set\\alpha,\\ s \\subseteq iUnion t} \\sum' n, \\inf_{\\mu \\in m} \\mu (t n) $$$
Lean4
/-- The value of the Infimum of a set of outer measures on a nonempty 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 : s.Nonempty) :
sInf m s = ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' n, ⨅ (μ : OuterMeasure α) (_ : μ ∈ m), μ (t n) :=
m.eq_empty_or_nonempty.elim (fun hm => by simp [hm, h]) sInf_apply
