Theorems · Definition · algebraic topology

ContinuousMap.HomotopyEquiv.mk.noConfusion

{X : Type u} →
  {Y : Type v} →
    {inst : TopologicalSpace X} →
      {inst_1 : TopologicalSpace Y} →
        {P : Sort u_1} →
          {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' : 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 := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
                              { toFun := toFun', invFun := invFun', left_inv := left_inv', right_inv := right_inv' } →
                            (toFun ≍ toFun' → invFun ≍ invFun' → P) → P

Defined in

Mathlib.Topology.Homotopy.Equiv

Cited by

1 results in Mathlib

Foundations

Depth 22 from the axioms · uses no axioms