English
If g and h belong to the connected component of the identity in a topological group G, then their product gh lies in the same connected component.
Русский
Если элементы g и h принадлежат компоненте связности единицы в топологической группе G, то произведение gh принадлежит той же компоненте.
LaTeX
$$$g,h \in \operatorname{connectedComponent}(1)\;\Rightarrow\; gh \in \operatorname{connectedComponent}(1)$$$
Lean4
@[to_additive]
theorem mul_mem_connectedComponent_one {G : Type*} [TopologicalSpace G] [MulOneClass G] [ContinuousMul G] {g h : G}
(hg : g ∈ connectedComponent (1 : G)) (hh : h ∈ connectedComponent (1 : G)) : g * h ∈ connectedComponent (1 : G) :=
by
rw [connectedComponent_eq hg]
have hmul : g ∈ connectedComponent (g * h) :=
by
apply Continuous.image_connectedComponent_subset (continuous_mul_left g)
rw [← connectedComponent_eq hh]
exact ⟨(1 : G), mem_connectedComponent, by simp only [mul_one]⟩
simpa [← connectedComponent_eq hmul] using mem_connectedComponent
