topologicalClosure_coe — Mathlib

English

The carrier of the topological closure of a subgroup equals the closure of its carrier as a subset of G.

Русский

Облако (мощность) замыкания подгруппы совпадает с замыканием её множества как подмножества G.

LaTeX

$$$(s.topologicalClosure : Set G) = \overline{(s : Set G)}$$$

Lean4

@[to_additive (attr := simp)]
theorem topologicalClosure_coe {s : Subgroup G} : (s.topologicalClosure : Set G) = _root_.closure s :=
  rfl

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