Theorems · Theorem · algebraic topology

ContinuousMap.HomotopyEquiv.mk.inj

∀ {X : Type u} {Y : Type v} {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y} {toFun : C(X, Y)}
  {invFun : C(Y, X)} {left_inv : (invFun.comp toFun).Homotopic (ContinuousMap.id X)}
  {right_inv : (toFun.comp invFun).Homotopic (ContinuousMap.id Y)} {toFun_1 : C(X, Y)} {invFun_1 : C(Y, X)}
  {left_inv_1 : (invFun_1.comp toFun_1).Homotopic (ContinuousMap.id X)}
  {right_inv_1 : (toFun_1.comp invFun_1).Homotopic (ContinuousMap.id Y)},
  { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 } →
    toFun = toFun_1 ∧ invFun = invFun_1

Defined in

Mathlib.Topology.Homotopy.Equiv

Cited by

1 results in Mathlib

Foundations

Depth 23 from the axioms · uses no axioms