isPiSystem_isClosed — Mathlib

English

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

Русский

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

LaTeX

$$$$ \forall s,t,\ (IsClosed(s) \land IsClosed(t)) \Rightarrow IsClosed(s \cap t). $$$$

Lean4

theorem isPiSystem_isClosed [TopologicalSpace α] : IsPiSystem ({s : Set α | IsClosed s}) := fun _s hs _t ht _ ↦
  IsClosed.inter hs ht

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