English
For any subset s of α, the restriction of the infimum over i of m_i to s equals the infimum over i of the restrictions to s: restrict s (⨅ i, m_i) = ⨅ i, restrict s (m_i).
Русский
Для подмножества s ⊆ α констатируем: ограничение инфимума по i на s равно инфимуму ограничений: 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_restrict {ι} (s : Set α) (m : ι → OuterMeasure α) :
restrict s (⨅ i, restrict s (m i)) = restrict s (⨅ i, m i) :=
calc
restrict s (⨅ i, restrict s (m i))
_ = restrict (range ((↑) : s → α)) (⨅ i, restrict s (m i)) := by rw [Subtype.range_coe]
_ = map ((↑) : s → α) (⨅ i, comap (↑) (m i)) := (map_iInf Subtype.coe_injective _).symm
_ = restrict s (⨅ i, m i) := congr_arg (map ((↑) : s → α)) (comap_iInf _ _).symm
