interior_biInter — Mathlib

English

For a finite index set S and a family f, interior of the finite intersection equals the finite intersection of interiors.

Русский

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

LaTeX

$$$ \forall S\text{ finite},\ \forall f:S \to \mathcal P(X),\ \operatorname{int}\left(\bigcap_{i \in S} f(i)\right) = \bigcap_{i \in S} \operatorname{int}(f(i))$$$

Lean4

theorem interior_biInter {ι : Type*} {s : Set ι} (hs : s.Finite) (f : ι → Set X) :
    interior (⋂ i ∈ s, f i) = ⋂ i ∈ s, interior (f i) := by
  induction s, hs using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ _ => simp [*]

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