interior_sInter_subset — Mathlib

English

For S a collection of sets, interior of the intersection over S is contained in the intersection of interiors over S.

Русский

Для множества S наборов: interior(⋂ S) ⊆ ⋂ s∈S interior(s).

LaTeX

$$$ \operatorname{int}(\bigcap_{s \in S} s) \subseteq \bigcap_{s \in S} \operatorname{int}(s)$$$

Lean4

theorem interior_sInter_subset (S : Set (Set X)) : interior (⋂₀ S) ⊆ ⋂ s ∈ S, interior s :=
  calc
    interior (⋂₀ S) = interior (⋂ s ∈ S, s) := by rw [sInter_eq_biInter]
    _ ⊆ ⋂ s ∈ S, interior s := interior_iInter₂_subset _ _

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