Theorems · Definition · Lie groups

Subgroup.topologicalClosure

{G : Type w} → [inst : TopologicalSpace G] → [inst_1 : Group G] → [IsTopologicalGroup G] → Subgroup G → Subgroup G

The (topological-space) closure of a subgroup of a topological group is itself a subgroup.

Defined in

Mathlib.Topology.Algebra.Group.Basic

Cited by

12 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceGroupIsTopologicalGroup