interior_sInter — Mathlib

English

For a finite set S 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

$$$ \forall S \subseteq \mathcal P(X),\ S\text{ finite} \Rightarrow \operatorname{int}\left(\bigcap_{s \in S} s\right) \subseteq \bigcap_{s \in S} \operatorname{int}(s)$$$

Lean4

theorem interior_sInter {S : Set (Set X)} (hS : S.Finite) : interior (⋂₀ S) = ⋂ s ∈ S, interior s := by
  rw [sInter_eq_biInter, hS.interior_biInter]

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