English
If ι is nonempty, then restricting the infimum of a family of outer measures to s equals the infimum of the restrictions: restrict s (⨅ i, m_i) = ⨅ i, restrict s (m_i).
Русский
Пусть индексы ι невырожденны. Тогда ограничение инфимума по i совпадает с инфимумом ограничений: restrict_s(⨅_i m_i) = ⨅_i restrict_s(m_i).
LaTeX
$$$\operatorname{restrict}_s\left(\bigwedge_{i} m_i\right) = \bigwedge_{i} \operatorname{restrict}_s(m_i).$$$
Lean4
theorem restrict_iInf {ι} [Nonempty ι] (s : Set α) (m : ι → OuterMeasure α) :
restrict s (⨅ i, m i) = ⨅ i, restrict s (m i) :=
(congr_arg (map ((↑) : s → α)) (comap_iInf _ _)).trans (map_iInf_comap _)