interior_iInter_of_finite — Mathlib

English

If the index type is finite, interior of the intersection over all i is the intersection of interiors.

Русский

Пусть ι конечен: interior(⋂ i, f(i)) = ⋂ i, interior(f(i)).

LaTeX

$$$ [Finite \iota] \ (f : \iota \to Set X) :\ interior (\bigcap_{i} f(i)) = \bigcap_{i} interior (f(i))$$$

Lean4

@[simp]
theorem interior_iInter_of_finite [Finite ι] (f : ι → Set X) : interior (⋂ i, f i) = ⋂ i, interior (f i) := by
  rw [← sInter_range, (finite_range f).interior_sInter, biInter_range]

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