English
Generalization: for a family of sets indexed by i, interior of the iterated intersection is contained in the iterated interiors.
Русский
Обобщение: для семейства множеств, индексируемого i, interior(⋂ i, s_i) ⊆ ⋂ i, interior(s_i).
LaTeX
$$$ \forall s : \iota \to Set X,\ interior(\bigcap_{i} s(i)) \subseteq \bigcap_{i} interior(s(i))$$$
Lean4
theorem interior_iInter₂_subset (p : ι → Sort*) (s : ∀ i, p i → Set X) :
interior (⋂ (i) (j), s i j) ⊆ ⋂ (i) (j), interior (s i j) :=
(interior_iInter_subset _).trans <| iInter_mono fun _ => interior_iInter_subset _