interior_iInter_subset — Mathlib

English

The interior of the intersection over a family is contained in the intersection of the interiors.

Русский

Интерьер пересечения семейства множеств содержится в пересечении их интерьеров.

LaTeX

$$$ \operatorname{int}\left( \bigcap_i s_i \right) \subseteq \bigcap_i \operatorname{int}(s_i)$$$

Lean4

theorem interior_iInter_subset (s : ι → Set X) : interior (⋂ i, s i) ⊆ ⋂ i, interior (s i) :=
  subset_iInter fun _ => interior_mono <| iInter_subset _ _

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