subsingleton_closure — Mathlib

English

In a T1-space, closure(s) is a subsingleton iff s is a subsingleton.

Русский

В T1-пространстве closure(s) является subsingleton тогда и только тогда, когда s является subsingleton.

LaTeX

$$$ (closure s).Subsingleton \iff s.Subsingleton $.$$

Lean4

@[simp]
theorem subsingleton_closure [T1Space X] {s : Set X} : (closure s).Subsingleton ↔ s.Subsingleton :=
  ⟨fun h => h.anti subset_closure, fun h => h.closure⟩

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