LeanPool.WhiteheadTheorem.Basic

Imported Lean Pool material for LeanPool.WhiteheadTheorem.Basic.

theorem WhiteheadTheorem (X Y : CWComplex) (f : X.toTopCat ⟶ Y.toTopCat) : IsWeakHomotopyEquiv (TopCat.Hom.hom f) → IsHomotopyEquiv (TopCat.Hom.hom f)