6.46. MappingDegree.PreconnectedFromFiniteComplement🔗

Jacobians.MappingDegree.PreconnectedFromFiniteComplement — source

isPreconnected_compl_finite_of_isPathConnected

Given the path-connectedness of Cᶜ, preconnectedness follows.

Used by RegularSubsetPreconnected.lean's h_topo parameter via the convenience wrapper isPreconnected_compl_of_isPathConnected_compl below.

theorem isPreconnected_compl_finite_of_isPathConnected
    {Y : Type u} [TopologicalSpace Y] [T1Space Y]
    {C : Set Y} (_hC : C.Finite)
    (h_path : (Cᶜ : Set Y).Nonempty → IsPathConnected (Cᶜ : Set Y)) :
    IsPreconnected (Cᶜ : Set Y)

isPreconnected_compl_of_isPathConnected_compl

Convenience composition. If the complement of every finite set is path-connected (when nonempty), then the complement of every finite set is preconnected — the shape consumed by RegularSubsetPreconnected.lean.

theorem isPreconnected_compl_of_isPathConnected_compl
    {Y : Type u} [TopologicalSpace Y] [T1Space Y]
    (h_path : ∀ C : Set Y, C.Finite → (Cᶜ : Set Y).Nonempty →
      IsPathConnected (Cᶜ : Set Y)) :
    ∀ C : Set Y, C.Finite → IsPreconnected (Cᶜ : Set Y)