Theorems · Definition · algebraic topology

ContinuousMap.HomotopicRel

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

Given continuous maps f₀ and f₁, we say f₀ and f₁ are homotopic relative to a set S if there exists a HomotopyRel f₀ f₁ S.

Defined in

Mathlib.Topology.Homotopy.Basic

Cited by

11 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpace