English
If m is defined on ι with nonempty domain, then the infimum over i of m i evaluated at s equals the infimum over all countable coverings t of s of the sum of innermost infima over i of m i (t n).
Русский
Если m задано на ι и s непусто, то инфимуим над i: m_i (s) равен инфимууму по покрытиям t, суммы инфимумов по i для каждого t(n).
LaTeX
$$$ (\\inf_i m_i)\\, s = \\inf_{t: \\mathbb{N} \\to Set\\alpha} \\inf_{x} \\sum' n, \\inf_i m_i (t n)$$$
Lean4
/-- The value of the Infimum of a family 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 iInf_apply' {ι} (m : ι → OuterMeasure α) {s : Set α} (hs : s.Nonempty) :
(⨅ i, m i) s = ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' n, ⨅ i, m i (t n) :=
by
rw [iInf, sInf_apply' hs]
simp only [iInf_range]
