Theorems · Theorem · algebraic topology

ContinuousMap.HomotopyEquiv.mk.injEq

∀ {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

0 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext

Assumes

TopologicalSpaceTopologicalSpace