Theorems · Definition · general topology

Path.add

{X : Type u_1} →
  [inst : TopologicalSpace X] →
    [inst_1 : Add X] → [ContinuousAdd X] → {a₁ b₁ a₂ b₂ : X} → Path a₁ b₁ → Path a₂ b₂ → Path (a₁ + a₂) (b₁ + b₂)

Pointwise addition of paths in a topological additive group.

Defined in

Mathlib.Topology.Path

Cited by

5 results in Mathlib

Foundations

Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceAddContinuousAdd