inv_mem_connectedComponent_one — Mathlib

English

The connected component of 1_G in a topological group G forms a subgroup of G.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem inv_mem_connectedComponent_one {G : Type*} [TopologicalSpace G] [DivisionMonoid G] [ContinuousInv G] {g : G}
    (hg : g ∈ connectedComponent (1 : G)) : g⁻¹ ∈ connectedComponent (1 : G) :=
  by
  rw [← inv_one]
  exact Continuous.image_connectedComponent_subset continuous_inv _ ((Set.mem_image _ _ _).mp ⟨g, hg, rfl⟩)

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