interior_iInter — Mathlib

English

For a finite index set ι and a family f(i) of sets, interior of the intersection over i is the intersection of interiors.

Русский

Для конечного множества индексов ι: interior(⋂ i∈ι f(i)) = ⋂ i∈ι interior(f(i)).

LaTeX

$$$ \forall X [TopologicalSpace X], \forall s:\text{ Finite}, \forall f:s \to Set X,\ \operatorname{int}\left(\bigcap_{i \in s} f(i)\right) = \bigcap_{i \in s} \operatorname{int}(f(i))$$$

Lean4

@[simp]
theorem interior_iInter {ι : Type*} (s : Finset ι) (f : ι → Set X) :
    interior (⋂ i ∈ s, f i) = ⋂ i ∈ s, interior (f i) :=
  s.finite_toSet.interior_biInter f

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