Theorems · Definition · algebraic topology

ContinuousMap.HomotopyEquiv.noConfusion

{P : Sort u_1} →
  {X : Type u} →
    {Y : Type v} →
      {inst : TopologicalSpace X} →
        {inst_1 : TopologicalSpace Y} →
          {t : ContinuousMap.HomotopyEquiv X Y} →
            {X' : Type u} →
              {Y' : Type v} →
                {inst' : TopologicalSpace X'} →
                  {inst'_1 : TopologicalSpace Y'} →
                    {t' : ContinuousMap.HomotopyEquiv X' Y'} →
                      X = X' →
                        Y = Y' →
                          inst ≍ inst' → inst_1 ≍ inst'_1 → t ≍ t' → ContinuousMap.HomotopyEquiv.noConfusionType P t t'

Defined in

Mathlib.Topology.Homotopy.Equiv

Cited by

0 results in Mathlib

Foundations

Depth 21 from the axioms · uses no axioms