Theorems · Definition · algebraic topology

FundamentalGroupoidFunctor.equivOfHomotopyEquiv

{X : Type u_3} →
  {Y : Type u_4} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        ContinuousMap.HomotopyEquiv X Y →
          (↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of X)) ≌
            ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of Y)))

Homotopy equivalent topological spaces have equivalent fundamental groupoids.

Defined in

Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Cited by

1 results in Mathlib

Foundations

Depth 142 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace