Locally convex spaces are strongly locally contractible

A real locally convex topological vector space has a basis of convex neighbourhoods at each point, and a nonempty convex set is contractible (Convex.contractibleSpace). Hence every point has a basis of contractible neighbourhoods: the space is strongly locally contractible.

Mathlib records the weaker consequence that such a space is locally path-connected (LocallyConvexSpace.toLocallyPathConnectedSpace); this file records the contractible version. Together with IsOpen.stronglyLocallyContractibleSpace it makes every open subset of a real normed space, such as a punctured plane, strongly locally contractible, and hence locally path-connected and semilocally simply connected.

@[instance 100]

instance LocallyConvexSpace.toStronglyLocallyContractibleSpace {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] : StronglyLocallyContractibleSpace E

A real locally convex space is strongly locally contractible: its convex neighbourhoods of a point are nonempty, hence contractible, and they form a basis of neighbourhoods.