isClosed_singleton_inter — Mathlib

English

In a T1 space, for any A and a, the intersection {a} ∩ A is closed.

Русский

В T1-пространстве для любого A и точки a пересечение {a} ∩ A замкнуто.

LaTeX

$$$ \\forall X\\ [TopologicalSpace X] [T1Space X], \\forall A \\subseteq X, \\forall a \\in X,\\ IsClosed({a} \\cap A). $$$

Lean4

theorem isClosed_singleton_inter [T1Space X] {A : Set X} {a : X} : IsClosed ({ a } ∩ A) :=
  Subsingleton.singleton_inter.isClosed

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