English
For a nonempty index set ι and a family of outer measures m i, the value at s of the infimum over i is the infimum over all countable coverings t of s of the sum of inner infima m i (t n).
Русский
Для непустого множества индексов ι и семейства внешних мер m_i, значение на s инфимума по i есть инфимуум по покрытиям t: s ⊆ ⋃ t(n) суммы по n инфимумов m_i (t(n)).
LaTeX
$$$(\\inf_i m_i)\\, s = \\inf_{t: \\mathbb{N} \\to Set\\alpha} (s \\subseteq iUnion t) \\sum' n, \\inf_i m_i (t n)$$$
Lean4
/-- The value of the Infimum of a nonempty family 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 iInf_apply {ι} [Nonempty ι] (m : ι → OuterMeasure α) (s : Set α) :
(⨅ i, m i) s = ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' n, ⨅ i, m i (t n) :=
by
rw [iInf, sInf_apply (range_nonempty m)]
simp only [iInf_range]
