6.43. MappingDegree.PathConnectedComplFinite🔗

Jacobians.MappingDegree.PathConnectedComplFinite — source

isPathConnected_compl_finite_of_connected_chartedSpace_complex

Main result. In a connected, T2 charted space modelled on ℂ (with the analytic-smoothness manifold structure available so that the statement type-checks at the natural level for downstream use), the complement of any finite set is path-connected, provided it is nonempty.

theorem isPathConnected_compl_finite_of_connected_chartedSpace_complex
    {Y : Type*} [TopologicalSpace Y] [ConnectedSpace Y] [T2Space Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    {C : Set Y} (hC_fin : C.Finite) (hC_compl : (Cᶜ : Set Y).Nonempty) :
    IsPathConnected (Cᶜ : Set Y)