restrict_iInf — Mathlib

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 _)

Похожие утверждения