isClosed_inter_singleton — Mathlib

English

In a T1 space, for any subset A and any point 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_inter_singleton [T1Space X] {A : Set X} {a : X} : IsClosed (A ∩ { a }) :=
  Subsingleton.inter_singleton.isClosed

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