Local contractibility of manifolds

Every point of a real manifold, possibly with boundary or corners, has a basis of contractible neighbourhoods. The model space H of a real model with corners I is homeomorphic to the convex set range I, whose intersections with balls are convex and hence contractible (ModelWithCorners.stronglyLocallyContractibleSpace), and a charted space inherits this property from its model through the inverse charts (ChartedSpace.stronglyLocallyContractibleSpace). The circle is an instance (instStronglyLocallyContractibleSpaceCircle).

In particular every point of a manifold has arbitrarily small open neighbourhoods whose inclusion is nullhomotopic, which is what makes small neighbourhoods of finitely many points categorical in the sense of Lusternik and Schnirelmann.

theorem ModelWithCorners.stronglyLocallyContractibleSpace {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) : StronglyLocallyContractibleSpace H

The model space of a real model with corners is strongly locally contractible: the model embeds it onto the convex set range I, in which every ball cuts out a convex, hence contractible, neighbourhood.

theorem ChartedSpace.stronglyLocallyContractibleSpace (H : Type u_1) [TopologicalSpace H] (M : Type u_2) [TopologicalSpace M] [ChartedSpace H M] [StronglyLocallyContractibleSpace H] : StronglyLocallyContractibleSpace M

A charted space modelled on a strongly locally contractible space is strongly locally contractible: the inverse chart at a point carries the contractible neighbourhoods of its coordinate inside the chart target onto contractible neighbourhoods of the point.

instance instStronglyLocallyContractibleSpaceCircle : StronglyLocallyContractibleSpace Circle

The circle is strongly locally contractible, as a manifold modelled on EuclideanSpace ℝ (Fin 1).