mul — Mathlib

English

If there is a path in s from a to b and a path in t from c to d, then there is a path in s·t from a·c to b·d (topological group setting).

Русский

Если существует путь в s от a к b и путь в t от c к d, то существует путь в s·t от a·c к b·d (в контексте топологической группы).

LaTeX

$$JoinedIn s a b → JoinedIn t c d → JoinedIn (s * t) (a * c) (b * d)$$

Lean4

@[to_additive]
theorem mul {M : Type*} [Mul M] [TopologicalSpace M] [ContinuousMul M] {s t : Set M} {a b c d : M} (hs : JoinedIn s a b)
    (ht : JoinedIn t c d) : JoinedIn (s * t) (a * c) (b * d) :=
  ⟨hs.somePath.mul ht.somePath, fun t ↦ Set.mul_mem_mul (hs.somePath_mem t) (ht.somePath_mem t)⟩

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