Affine homotopy between two continuous maps

In this file we define ContinuousMap.Homotopy.affine f g to be the homotopy between f and g such that affine f g (t, x) = AffineMap.lineMap (f x) (g x) t.

def ContinuousMap.Homotopy.affine {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [Module ℝ E] [ContinuousSMul ℝ E] (f g : C(X, E)) : f.Homotopy g

The homotopy between f and g such that affine f g (t, x) = AffineMap.lineMap (f x) (g x) t.

Equations

• ContinuousMap.Homotopy.affine f g = { toFun := fun (x : ↑unitInterval × X) => (Path.segment (f x.2) (g x.2)) x.1, continuous_toFun := ⋯, map_zero_left := ⋯, map_one_left := ⋯ }

@[simp]

theorem ContinuousMap.Homotopy.affine_apply {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [Module ℝ E] [ContinuousSMul ℝ E] (f g : C(X, E)) (x : ↑unitInterval × X) : (affine f g) x = (AffineMap.lineMap (f x.2) (g x.2)) ↑x.1

@[simp]

theorem ContinuousMap.Homotopy.evalAt_affine {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [Module ℝ E] [ContinuousSMul ℝ E] (f g : C(X, E)) (x : X) : (affine f g).evalAt x = Path.segment (f x) (g x)