connectedComponentOfOne — Mathlib

English

The connected component of 1_G is a subgroup of G.

Русский

Связанная компонента единицы 1_G образует подгруппу группы G.

LaTeX

$$$\operatorname{connectedComponentOfOne}(G) \le G$$$

Lean4

/-- The connected component of 1 is a subgroup of `G`. -/
@[to_additive /-- The connected component of 0 is a subgroup of `G`. -/
    ]
def connectedComponentOfOne (G : Type*) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : Subgroup G
    where
  carrier := connectedComponent (1 : G)
  one_mem' := mem_connectedComponent
  mul_mem' hg hh := mul_mem_connectedComponent_one hg hh
  inv_mem' hg := inv_mem_connectedComponent_one hg

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