English
In a topological group, the path component of the identity forms a subgroup.
Русский
В топологической группе компонент пути единицы образует подгруппу.
LaTeX
$$$$\text{Let } G \text{ be a topological group. Then } \operatorname{pathComponentOne}(G) \text{ is a subgroup of } G,$$ i.e. $$1_G \in \operatorname{pathComponentOne}(G) \land \forall g,h \in \operatorname{pathComponentOne}(G),\ g h \in \operatorname{pathComponentOne}(G).$$$$
Lean4
/-- The path component of the identity in a topological group, as a subgroup. -/
@[to_additive (attr := simps!) /-- The path component of the identity in an additive topological
group, as an additive subgroup. -/
]
def pathComponentOne (G : Type*) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Subgroup G
where
toSubmonoid := .pathComponentOne G
inv_mem' {g} hg := by simpa using hg.inv
