English
In a topological group, pointwise multiplication of paths is defined by composing the product of endpoints: (γ1.mul γ2)(t) = γ1(t) · γ2(t).
Русский
В топологической группе по точкам определяется умножение путей: (γ1.mul γ2)(t) = γ1(t) γ2(t).
LaTeX
$$$(\gamma_1 \cdot \gamma_2)(t) = \gamma_1(t) \cdot \gamma_2(t).$$$
Lean4
/-- Pointwise multiplication of paths in a topological group. -/
@[to_additive (attr := simps!) /-- Pointwise addition of paths in a topological additive group. -/
]
protected def mul [Mul X] [ContinuousMul X] {a₁ b₁ a₂ b₂ : X} (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) :
Path (a₁ * a₂) (b₁ * b₂) :=
(γ₁.prod γ₂).map continuous_mul
