restrict_biInf — Mathlib

English

For a nonempty I ⊆ ι, the restriction to s distributes over the infimum taken over i∈I: restrict s (⨅ i∈I, m_i) = ⨅ i∈I, restrict s (m_i).

Русский

Для непустого I ⊆ ι ограничение по s распределяется над инфимумом по i∈I: restrict_s(⨅_{i∈I} m_i) = ⨅_{i∈I} restrict_s(m_i).

LaTeX

$$$\operatorname{restrict}_s\left(\bigwedge_{i\in I} m_i\right) = \bigwedge_{i\in I} \operatorname{restrict}_s(m_i).$$$

Lean4

theorem restrict_biInf {ι} {I : Set ι} (hI : I.Nonempty) (s : Set α) (m : ι → OuterMeasure α) :
    restrict s (⨅ i ∈ I, m i) = ⨅ i ∈ I, restrict s (m i) :=
  by
  haveI := hI.to_subtype
  rw [← iInf_subtype'', ← iInf_subtype'']
  exact restrict_iInf _ _

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