interior_iInter₂_subset — Mathlib

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 _

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