Locally path-connected spaces

This file defines LocPathConnectedSpace X, a predicate class asserting that X is locally path-connected, in that each point has a basis of path-connected neighborhoods.

Main results

• IsOpen.pathComponent / IsClosed.pathComponent: in locally path-connected spaces, path-components are both open and closed.
• pathComponent_eq_connectedComponent: in locally path-connected spaces, path-components and connected components agree.
• pathConnectedSpace_iff_connectedSpace: locally path-connected spaces are path-connected iff they are connected.
• instLocallyConnectedSpace: locally path-connected spaces are also locally connected.
• IsOpen.locPathConnectedSpace: open subsets of locally path-connected spaces are locally path-connected.
• LocPathConnectedSpace.coinduced / Quotient.locPathConnectedSpace: quotients of locally path-connected spaces are locally path-connected.
• Sum.locPathConnectedSpace / Sigma.locPathConnectedSpace: disjoint unions of locally path-connected spaces are locally path-connected.

Abstractly, this also shows that locally path-connected spaces form a coreflective subcategory of the category of topological spaces, although we do not prove that in this form here.

Implementation notes

In the definition of LocPathConnectedSpace X we require neighbourhoods in the basis to be path-connected, but not necessarily open; that they can also be required to be open is shown as a theorem in isOpen_isPathConnected_basis.

class LocPathConnectedSpace (X : Type u_4) [TopologicalSpace X] : Prop

A topological space is locally path connected, at every point, path connected neighborhoods form a neighborhood basis.

• path_connected_basis (x : X) : (nhds x).HasBasis (fun (s : Set X) => s ∈ nhds x ∧ IsPathConnected s) id

  Each neighborhood filter has a basis of path-connected neighborhoods.

theorem LocPathConnectedSpace.of_bases {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} {p : X → ι → Prop} {s : X → ι → Set X} (h : ∀ (x : X), (nhds x).HasBasis (p x) (s x)) (h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)) : LocPathConnectedSpace X

theorem IsOpen.pathComponentIn {X : Type u_1} [TopologicalSpace X] {F : Set X} [LocPathConnectedSpace X] (hF : IsOpen F) (x : X) : IsOpen (pathComponentIn F x)

theorem IsOpen.pathComponent {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] (x : X) : IsOpen (pathComponent x)

In a locally path connected space, each path component is an open set.

theorem IsClosed.pathComponent {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] (x : X) : IsClosed (pathComponent x)

In a locally path connected space, each path component is a closed set.

theorem IsClopen.pathComponent {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] (x : X) : IsClopen (pathComponent x)

In a locally path connected space, each path component is a clopen set.

theorem pathComponentIn_mem_nhds {X : Type u_1} [TopologicalSpace X] {x : X} {F : Set X} [LocPathConnectedSpace X] (hF : F ∈ nhds x) : pathComponentIn F x ∈ nhds x

theorem pathConnectedSpace_iff_connectedSpace {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] : PathConnectedSpace X ↔ ConnectedSpace X

theorem pathComponent_eq_connectedComponent {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] (x : X) : pathComponent x = connectedComponent x

theorem pathConnected_subset_basis {X : Type u_1} [TopologicalSpace X] {x : X} [LocPathConnectedSpace X] {U : Set X} (h : IsOpen U) (hx : x ∈ U) : (nhds x).HasBasis (fun (s : Set X) => s ∈ nhds x ∧ IsPathConnected s ∧ s ⊆ U) id

theorem isOpen_isPathConnected_basis {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] (x : X) : (nhds x).HasBasis (fun (s : Set X) => IsOpen s ∧ x ∈ s ∧ IsPathConnected s) id

theorem Topology.IsOpenEmbedding.locPathConnectedSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocPathConnectedSpace X] {e : Y → X} (he : IsOpenEmbedding e) : LocPathConnectedSpace Y

theorem IsOpen.locPathConnectedSpace {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] {U : Set X} (h : IsOpen U) : LocPathConnectedSpace ↑U

theorem IsOpen.isConnected_iff_isPathConnected {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] {U : Set X} (U_op : IsOpen U) : IsConnected U ↔ IsPathConnected U

instance instLocallyConnectedSpace {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] : LocallyConnectedSpace X

Locally path-connected spaces are locally connected.

theorem locPathConnectedSpace_iff_isOpen_pathComponentIn {X : Type u_4} [TopologicalSpace X] : LocPathConnectedSpace X ↔ ∀ (x : X) (u : Set X), IsOpen u → IsOpen (pathComponentIn u x)

A space is locally path-connected iff all path components of open subsets are open.

theorem locPathConnectedSpace_iff_pathComponentIn_mem_nhds {X : Type u_4} [TopologicalSpace X] : LocPathConnectedSpace X ↔ ∀ (x : X) (u : Set X), IsOpen u → x ∈ u → pathComponentIn u x ∈ nhds x

A space is locally path-connected iff all path components of open subsets are neighbourhoods.

theorem LocPathConnectedSpace.coinduced {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] {Y : Type u_4} (f : X → Y) : LocPathConnectedSpace Y

Any topology coinduced by a locally path-connected topology is locally path-connected.

theorem Topology.IsQuotientMap.locPathConnectedSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocPathConnectedSpace X] {f : X → Y} (h : IsQuotientMap f) : LocPathConnectedSpace Y

Quotients of locally path-connected spaces are locally path-connected.

instance Quot.locPathConnectedSpace {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] {r : X → X → Prop} : LocPathConnectedSpace (Quot r)

Quotients of locally path-connected spaces are locally path-connected.

instance Quotient.locPathConnectedSpace {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] {s : Setoid X} : LocPathConnectedSpace (Quotient s)

Quotients of locally path-connected spaces are locally path-connected.

instance Sum.locPathConnectedSpace {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] [LocPathConnectedSpace X] [LocPathConnectedSpace Y] : LocPathConnectedSpace (X ⊕ Y)

Disjoint unions of locally path-connected spaces are locally path-connected.

instance Sigma.locPathConnectedSpace {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), LocPathConnectedSpace (X i)] : LocPathConnectedSpace ((i : ι) × X i)

Disjoint unions of locally path-connected spaces are locally path-connected.

instance AlexandrovDiscrete.locPathConnectedSpace {X : Type u_1} [TopologicalSpace X] [AlexandrovDiscrete X] : LocPathConnectedSpace X