Joining_Paths_makes_Another_Path
Provedpath-connected-setsproofwikitopology
Let f, g be paths in a topological space T from a to b and from b to c respectively. Then the join of f and g is a path from a to c.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Topology.Connected.PathConnected
Formal statement
theorem Joining_Paths_makes_Another_Path {X : Type _} [TopologicalSpace X] {a b c : X} (f : Path a b) (g : Path b c) : ∃ h : Path a c, True := by sorrySource