interior_iInter — Mathlib

English

Interior commutes with arbitrary intersections: interior of the intersection equals the intersection of the interiors.

Русский

Interior сохраняется при произвольном пересечении: interior(∩ f_i) = ∩ interior(f_i).

LaTeX

$$$\forall (f:\text{⋯})\; \operatorname{interior}(\bigcap_i f_i) = \bigcap_i \operatorname{interior}(f_i)$$$

Lean4

theorem interior_iInter (f : ι → Set α) : interior (⋂ i, f i) = ⋂ i, interior (f i) :=
  (interior_maximal (iInter_mono fun _ ↦ interior_subset) <| isOpen_iInter fun _ ↦ isOpen_interior).antisymm' <|
    subset_iInter fun _ ↦ interior_mono <| iInter_subset _ _

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