Theorems · Theorem · algebraic topology

Path.Homotopic.map_trans_evalAt

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f g : C(X, Y)}
  (F : f.Homotopy g) {x₁ x₂ : X} (p : Path x₁ x₂),
  ((p.map ⋯).trans (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))

Let F be a homotopy between two continuous maps f g : C(X, Y). Given a path p : Path x₁ x₂ in the domain, consider the following two paths in the codomain. One path goes along the image of p under f, then along the trajectory of x₂ under F. The other path goes along the trajectory of x₁ under F, then along the image of p under g. These two paths are homotopic.

Defined in

Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace