Theorems · Inductive type · algebraic topology

ContinuousMap.Homotopy

{X : Type u} →
  {Y : Type v} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → C(X, Y) → C(X, Y) → Type (max u v)

ContinuousMap.Homotopy f₀ f₁ is the type of homotopies from f₀ to f₁. When possible, instead of parametrizing results over (f : ContinuousMap.Homotopy f₀ f₁), you should parametrize over {F : Type*} [HomotopyLike F f₀ f₁] (f : F). When you extend this structure, make sure to extend ContinuousMap.HomotopyLike.

Defined in

Mathlib.Topology.Homotopy.Basic

Cited by

65 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpace