feat(topology/[continuous_function, path_connected]): add bundled ver…

…sions of prod_mk and prod_map (#10512)

I also added a definition for pointwise addition of paths, but I'm not sure it would be really useful in general (my use case is the Sphere eversion project, where I need to add together two paths living in complement subspaces of a real TVS).

src/topology/continuous_function/basic.lean

@@ -211,6 +211,26 @@ end inf'
 
 end lattice
 
+section prod
+
+variables {α₁ α₂ β₁ β₂ : Type*}
+
+/-- Given two continuous maps `f` and `g`, this is the continuous map `x ↦ (f x, g x)`. -/
+def prod_mk {α β₁ β₂ : Type*} [topological_space α] [topological_space β₁]
+  [topological_space β₂] (f : C(α, β₁)) (g : C(α, β₂)) :
+  C(α, β₁ × β₂) :=
+{ to_fun := (λ x, (f x, g x)),
+  continuous_to_fun := continuous.prod_mk f.continuous g.continuous }
+
+/-- Given two continuous maps `f` and `g`, this is the continuous map `(x, y) ↦ (f x, g y)`. -/
+def prod_map {α₁ α₂ β₁ β₂ : Type*} [topological_space α₁] [topological_space α₂]
+  [topological_space β₁] [topological_space β₂] (f : C(α₁, α₂)) (g : C(β₁, β₂)) :
+  C(α₁ × β₁, α₂ × β₂) :=
+{ to_fun := prod.map f g,
+  continuous_to_fun := continuous.prod_map f.continuous g.continuous }
+
+end prod
+
 section restrict
 
 variables (s : set α)

src/topology/path_connected.lean

@@ -372,6 +372,28 @@ begin
     simp [hst, mul_inv_cancel (@two_ne_zero ℝ _ _)] }
 end
 
+/-! #### Product of two paths -/
+
+/-- Given a path in `X` and a path in `Y`, we can take their pointwise product to get a path in
+`X × Y`. -/
+protected def prod {a₁ b₁ : X} {a₂ b₂ : Y} (γ₁ : path a₁ b₁) (γ₂ : path a₂ b₂) :
+  path (a₁, a₂) (b₁, b₂) :=
+{ to_continuous_map := continuous_map.prod_mk γ₁.to_continuous_map γ₂.to_continuous_map,
+  source' := by dsimp [continuous_map.prod_mk]; rwa [γ₁.source, γ₂.source],
+  target' := by dsimp [continuous_map.prod_mk]; rwa [γ₁.target, γ₂.target] }
+
+/-! #### Pointwise multiplication/addition of two paths in a topological (additive) group -/
+
+/-- Pointwise multiplication of paths in a topological group. The additive version is probably more
+useful. -/
+@[to_additive "Pointwise addition of paths in a topological additive group. -/"]
+protected def mul [has_mul X] [has_continuous_mul X] {a₁ b₁ a₂ b₂ : X}
+  (γ₁ : path a₁ b₁) (γ₂ : path a₂ b₂) : path (a₁ * a₂) (b₁ * b₂) :=
+(γ₁.prod γ₂).map continuous_mul
+
+@[to_additive] protected lemma mul_apply [has_mul X] [has_continuous_mul X] {a₁ b₁ a₂ b₂ : X}
+  (γ₁ : path a₁ b₁) (γ₂ : path a₂ b₂) (t : unit_interval) : (γ₁.mul γ₂) t = γ₁ t * γ₂ t := rfl
+
 /-! #### Truncating a path -/
 
 /-- `γ.truncate t₀ t₁` is the path which follows the path `γ` on the