Theorems · Definition · algebraic topology

ContinuousMap.HomotopyWith.symm

{X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {P : C(X, Y) → Prop} → {f₀ f₁ : C(X, Y)} → f₀.HomotopyWith f₁ P → f₁.HomotopyWith f₀ P

Given a HomotopyWith f₀ f₁ P, we can define a HomotopyWith f₁ f₀ P by reversing the homotopy.

Defined in

Mathlib.Topology.Homotopy.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace