LeanPool.WhiteheadTheorem.Defs

Imported Lean Pool material for LeanPool.WhiteheadTheorem.Defs.

def IsWeakHomotopyEquiv {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : Prop

IsWeakHomotopyEquiv

Equations

• IsWeakHomotopyEquiv f = (Nonempty X ∧ ∀ (n : ℕ) (x : X), Function.Bijective (HomotopyGroup.inducedMap n x f))

theorem isIso_inducedPointedHom_of_isWeakHomotopyEquiv {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} (hf : IsWeakHomotopyEquiv f) (n : ℕ) (x : X) : CategoryTheory.IsIso (HomotopyGroup.inducedPointedHom n x f)

def IsHomotopyEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : Prop

IsHomotopyEquiv

Equations

• IsHomotopyEquiv f = ∃ (equiv : ContinuousMap.HomotopyEquiv X Y), equiv.toFun = f