isOpen_sInter — Mathlib

English

Arbitrary intersections of open sets are open in Alexandrov discrete spaces: if every member of a collection S is open, then their intersection is open.

Русский

Произвольные пересечения открытых множеств открыты в пространстве Александрова-дискретного типа: если каждое множество из семейства S открыто, то их пересечение открыто.

LaTeX

$$$\Big(\forall s\in S, \ IsOpen(s)\Big) \Rightarrow IsOpen(\bigcap S)$$$

Lean4

theorem isOpen_sInter : (∀ s ∈ S, IsOpen s) → IsOpen (⋂₀ S) :=
  AlexandrovDiscrete.isOpen_sInter _

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