6.14. MappingDegree.ChartedSpaceLocPathConnected🔗

Jacobians.MappingDegree.ChartedSpaceLocPathConnected — source

instLocPathConnectedSpace_complex

ℂ, viewed as an ℝ-normed space, is locally path-connected.

instance instLocPathConnectedSpace_complex : LocPathConnectedSpace ℂ

locPathConnectedSpace_of_chartedSpace_complex

Any topological space charted on ℂ is locally path-connected.

theorem locPathConnectedSpace_of_chartedSpace_complex
    {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y] :
    LocPathConnectedSpace Y