Theorems · Inductive type · algebraic topology

ContinuousMap.HomotopyEquiv

(X : Type u) → (Y : Type v) → [TopologicalSpace X] → [TopologicalSpace Y] → Type (max u v)

A homotopy equivalence between topological spaces X and Y are a pair of functions toFun : C(X, Y) and invFun : C(Y, X) such that toFun.comp invFun and invFun.comp toFun are both homotopic to corresponding identity maps.

Defined in

Mathlib.Topology.Homotopy.Equiv

Cited by

23 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpace