coe_topologicalClosure_bot — Mathlib

English

The topological closure of the trivial subgroup equals the closure of the singleton {1}.

Русский

Топологическое замыкание тривиальной подгруппы равно замыканию множества {1}.

LaTeX

$$$\big( (\perp : Subgroup G) .topologicalClosure \big) : Set G = \overline{\{1\}}$$$

Lean4

@[to_additive]
theorem coe_topologicalClosure_bot : ((⊥ : Subgroup G).topologicalClosure : Set G) = _root_.closure ({ 1 } : Set G) :=
  by simp

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