pathComponentOne — Mathlib

English

The path component of the identity in a topological group is a normal subgroup.

Русский

Компонента пути единицы в топологической группе образует нормальную подгруппу.

LaTeX

$$$$\text{In a topological group } G,\ \operatorname{pathComponentOne}(G) \trianglelefteq G.$$$$

Lean4

/-- The path component of the identity in a topological group is normal. -/
@[to_additive]
instance pathComponentOne (G : Type*) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    (Subgroup.pathComponentOne G).Normal where
  conj_mem _ := fun ⟨γ⟩ g ↦ ⟨⟨⟨(g * γ · * g⁻¹), by fun_prop⟩, by simp, by simp⟩⟩

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