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 _ _