Theorems · Definition · algebraic topology

ContinuousMap.HomotopyRel.refl

{X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → (f : C(X, Y)) → (S : Set X) → f.HomotopyRel f S

Given a map f : C(X, Y) and a set S, we can define a HomotopyRel f f S by setting F (t, x) = f x for all t. This is defined using HomotopyWith.refl, but with the proof filled in.

Defined in

Mathlib.Topology.Homotopy.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace