Theorems · Theorem · algebraic topology

ContinuousMap.HomotopyEquiv.left_inv

∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (self : ContinuousMap.HomotopyEquiv X Y), (self.invFun.comp self.toFun).Homotopic (ContinuousMap.id X)

Defined in

Mathlib.Topology.Homotopy.Equiv

Cited by

1 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpace