mul — Mathlib

English

In a topological monoid, if a path joins a to b and a path joins c to d, then their product path joins a c to b d.

Русский

В топологической группе/полугруппе с непрерывной операцией плавно складываются пути: если есть путь a→b и путь c→d, то есть путь a·c→b·d.

LaTeX

$$$Joined a b \to Joined c d \Rightarrow Joined (a*c) (b*d)$$$

Lean4

@[to_additive]
theorem mul {M : Type*} [Mul M] [TopologicalSpace M] [ContinuousMul M] {a b c d : M} (hs : Joined a b)
    (ht : Joined c d) : Joined (a * c) (b * d) :=
  ⟨hs.somePath.mul ht.somePath⟩

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