English
If s and t are path-connected subsets of a topological space with a binary operation, then s·t is path-connected.
Русский
Если s и t — связанные по траекториям подмножества пространства с бинарной операцией, то s·t связано по траекториям.
LaTeX
$$$$\text{If } s,t \text{ are path-connected in a topological monoid}, \ s t \text{ is path-connected}.$$$$
Lean4
@[to_additive]
theorem mul {M : Type*} [Mul M] [TopologicalSpace M] [ContinuousMul M] {s t : Set M} (hs : IsPathConnected s)
(ht : IsPathConnected t) : IsPathConnected (s * t) :=
let ⟨a, ha_mem, ha⟩ := hs;
let ⟨b, hb_mem, hb⟩ := ht
⟨a * b, mul_mem_mul ha_mem hb_mem, Set.forall_mem_image2.2 fun _x hx _y hy ↦ (ha hx).mul (hb hy)⟩
