Theorems · Inductive type · general topology

StronglyLocallyContractibleSpace

(X : Type u_4) → [TopologicalSpace X] → Prop

A topological space is strongly locally contractible if, at every point, contractible neighborhoods form a neighborhood basis. Here "contractible" means contractible as a subspace. This is strictly stronger than the classical notion of locally contractible, which only requires null-homotopic inclusions. This distinction is witnessed by an example from Borsuk-Mazurkiewicz [borsuk_mazurkiewicz1934]; see also [MO88628] for discussion and the Whitehead manifold example.

Defined in

Mathlib.Topology.Homotopy.LocallyContractible

Cited by

6 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpace