English
For a nonempty I ⊆ ι and family m_i, the infimum over i ∈ I of m_i evaluated on s equals the infimum over countable coverings t of s of the sum of inner infima m_i (t n) over i ∈ I.
Русский
Для непустого множества I ⊆ ι и семейства мер m_i, инфимуум по i ∈ I на s равен инфимууму по покрытиям t суммы инфимумов по i ∈ I на t(n).
LaTeX
$$$ (\\inf_{i \\in I} m_i)\\, s = \\inf_{t: \\mathbb{N} \\to Set\\alpha} \\left( s \\subseteq iUnion t \\right) \\sum' n, \\inf_{i \\in 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 biInf_apply {ι} {I : Set ι} (hI : I.Nonempty) (m : ι → OuterMeasure α) (s : Set α) :
(⨅ i ∈ I, m i) s = ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' n, ⨅ i ∈ I, m i (t n) :=
by
haveI := hI.to_subtype
simp only [← iInf_subtype'', iInf_apply]
