Convex sets are locally path-connected #
A convex subset s of a real topological vector space is locally path-connected
(Convex.locallyPathConnectedSpace'). The neighbourhoods in s of a point x ∈ s of the form
s ∩ (x + W), with W a balanced neighbourhood of zero, form a basis, and each of them is
star-convex about x, hence path-connected.
Mathlib's Convex.locallyPathConnectedSpace proves this for locally convex spaces only; balanced
neighbourhoods of zero exist in every real topological vector space, so local convexity is not
needed. This covers, for instance, convex subsets of the spaces Lᵖ with 0 < p < 1, which are
not locally convex.
theorem
Convex.locallyPathConnectedSpace'
{E : Type u_1}
[AddCommGroup E]
[Module ℝ E]
[TopologicalSpace E]
[IsTopologicalAddGroup E]
[ContinuousSMul ℝ E]
{s : Set E}
(hs : Convex ℝ s)
:
A convex subset of a real topological vector space is locally path-connected.