isPiSystem_isOpen — Mathlib

English

In any topological space α, the family of open sets forms a Pi-system: the intersection of any two open sets is open.

Русский

В любом топологическом пространстве α множество открытых множеств образует пи-систему: пересечение любых двух открытых множеств является открытым.

LaTeX

$$$$ \forall s,t \subseteq \alpha,\ (IsOpen(s) \land IsOpen(t)) \Rightarrow IsOpen(s \cap t). $$$$

Lean4

theorem isPiSystem_isOpen [TopologicalSpace α] : IsPiSystem ({s : Set α | IsOpen s}) := fun _s hs _t ht _ =>
  IsOpen.inter hs ht

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