Documentation

Mathlib.Topology.Connected.LocallyPathConnected

Locally path-connected spaces #

This file defines LocallyPathConnectedSpace 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.locallyPathConnectedSpace: open subsets of locally path-connected spaces are locally path-connected.
LocallyPathConnectedSpace.coinduced / Quotient.locallyPathConnectedSpace: quotients of locally path-connected spaces are locally path-connected.
Sum.locallyPathConnectedSpace / Sigma.locallyPathConnectedSpace: 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 LocallyPathConnectedSpace 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 LocallyPathConnectedSpace (X : Type u_4) [TopologicalSpace X] :

A topological space is locally path connected if, 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.

Instances

@[deprecated LocallyPathConnectedSpace (since := "2026-06-21")]

def LocPathConnectedSpace (X : Type u_4) [TopologicalSpace X] :

Alias of LocallyPathConnectedSpace.

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

Equations

LocPathConnectedSpace = LocallyPathConnectedSpace

Instances For

@[deprecated LocallyPathConnectedSpace.path_connected_basis (since := "2026-06-21")]

theorem LocPathConnectedSpace.path_connected_basis {X : Type u_4} {inst✝ : TopologicalSpace X} [self : LocallyPathConnectedSpace X] (x : X) :

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

Alias of LocallyPathConnectedSpace.path_connected_basis.

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

theorem LocallyPathConnectedSpace.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)) :

LocallyPathConnectedSpace X

@[deprecated LocallyPathConnectedSpace.of_bases (since := "2026-06-21")]

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)) :

LocallyPathConnectedSpace X

Alias of LocallyPathConnectedSpace.of_bases.

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

IsOpen (pathComponentIn F x)

theorem IsOpen.pathComponent {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace 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] [LocallyPathConnectedSpace 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] [LocallyPathConnectedSpace 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} [LocallyPathConnectedSpace X] (hF : F ∈ nhds x) :

pathComponentIn F x ∈ nhds x

theorem PathConnectedSpace.of_locallyPathConnectedSpace {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [ConnectedSpace X] :

PathConnectedSpace X

@[deprecated PathConnectedSpace.of_locallyPathConnectedSpace (since := "2026-06-21")]

theorem PathConnectedSpace.of_locPathConnectedSpace {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [ConnectedSpace X] :

PathConnectedSpace X

Alias of PathConnectedSpace.of_locallyPathConnectedSpace.

theorem pathConnectedSpace_iff_connectedSpace {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] :

PathConnectedSpace X ↔ ConnectedSpace X

theorem pathComponent_eq_connectedComponent {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] (x : X) :

pathComponent x = connectedComponent x

theorem connectedComponent_eq_iff_joined {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] (x y : X) :

connectedComponent x = connectedComponent y ↔ Joined x y

theorem connectedComponentSetoid_eq_pathSetoid {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] :

connectedComponentSetoid X = pathSetoid X

def connectedComponentsEquivZerothHomotopy {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] :

ConnectedComponents X ≃ ZerothHomotopy X

In a locally path-connected space, connected components and path-connected components align

Equations

connectedComponentsEquivZerothHomotopy = { toFun := Quotient.map id ⋯, invFun := ZerothHomotopy.toConnectedComponents, left_inv := ⋯, right_inv := ⋯ }

Instances For

@[simp]

theorem connectedComponentsEquivZerothHomotopy_apply {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] (x : X) :

connectedComponentsEquivZerothHomotopy ⟦x⟧ = ZerothHomotopy.mk x

@[simp]

theorem coe_connectedComponentsEquivZerothHomotopy_symm {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] :

⇑connectedComponentsEquivZerothHomotopy.symm = ZerothHomotopy.toConnectedComponents

theorem connectedComponentsEquivZerothHomotopy_symm_apply {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] (x : X) :

connectedComponentsEquivZerothHomotopy.symm (ZerothHomotopy.mk x) = ⟦x⟧

theorem pathConnected_subset_basis {X : Type u_1} [TopologicalSpace X] {x : X} [LocallyPathConnectedSpace 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] [LocallyPathConnectedSpace X] (x : X) :

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

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

LocallyPathConnectedSpace Y

@[deprecated Topology.IsOpenEmbedding.locallyPathConnectedSpace (since := "2026-06-21")]

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

LocallyPathConnectedSpace Y

Alias of Topology.IsOpenEmbedding.locallyPathConnectedSpace.

theorem IsOpen.locallyPathConnectedSpace {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] {U : Set X} (h : IsOpen U) :

LocallyPathConnectedSpace ↑U

@[deprecated IsOpen.locallyPathConnectedSpace (since := "2026-06-21")]

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

LocallyPathConnectedSpace ↑U

Alias of IsOpen.locallyPathConnectedSpace.

theorem IsOpen.isConnected_iff_isPathConnected {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] {U : Set X} (U_op : IsOpen U) :

IsConnected U ↔ IsPathConnected U

instance instLocallyConnectedSpace {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] :

LocallyConnectedSpace X

Locally path-connected spaces are locally connected.

theorem locallyPathConnectedSpace_iff_isOpen_pathComponentIn {X : Type u_4} [TopologicalSpace X] :

LocallyPathConnectedSpace 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.

@[deprecated locallyPathConnectedSpace_iff_isOpen_pathComponentIn (since := "2026-06-21")]

theorem locPathConnectedSpace_iff_isOpen_pathComponentIn {X : Type u_4} [TopologicalSpace X] :

LocallyPathConnectedSpace X ↔ ∀ (x : X) (u : Set X), IsOpen u → IsOpen (pathComponentIn u x)

Alias of locallyPathConnectedSpace_iff_isOpen_pathComponentIn.

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

theorem locallyPathConnectedSpace_iff_pathComponentIn_mem_nhds {X : Type u_4} [TopologicalSpace X] :

LocallyPathConnectedSpace 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.

@[deprecated locallyPathConnectedSpace_iff_pathComponentIn_mem_nhds (since := "2026-06-21")]

theorem locPathConnectedSpace_iff_pathComponentIn_mem_nhds {X : Type u_4} [TopologicalSpace X] :

LocallyPathConnectedSpace X ↔ ∀ (x : X) (u : Set X), IsOpen u → x ∈ u → pathComponentIn u x ∈ nhds x

Alias of locallyPathConnectedSpace_iff_pathComponentIn_mem_nhds.

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

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

LocallyPathConnectedSpace Y

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

@[deprecated LocallyPathConnectedSpace.coinduced (since := "2026-06-21")]

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

LocallyPathConnectedSpace Y

Alias of LocallyPathConnectedSpace.coinduced.

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

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

LocallyPathConnectedSpace Y

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

@[deprecated Topology.IsQuotientMap.locallyPathConnectedSpace (since := "2026-06-21")]

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

LocallyPathConnectedSpace Y

Alias of Topology.IsQuotientMap.locallyPathConnectedSpace.

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

instance Quot.locallyPathConnectedSpace {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] {r : X → X → Prop} :

LocallyPathConnectedSpace (Quot r)

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

@[deprecated Quot.locallyPathConnectedSpace (since := "2026-06-21")]

theorem Quot.locPathConnectedSpace {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] {r : X → X → Prop} :

LocallyPathConnectedSpace (Quot r)

Alias of Quot.locallyPathConnectedSpace.

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

instance Quotient.locallyPathConnectedSpace {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] {s : Setoid X} :

LocallyPathConnectedSpace (Quotient s)

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

@[deprecated Quotient.locallyPathConnectedSpace (since := "2026-06-21")]

theorem Quotient.locPathConnectedSpace {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] {s : Setoid X} :

LocallyPathConnectedSpace (Quotient s)

Alias of Quotient.locallyPathConnectedSpace.

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

instance Sum.locallyPathConnectedSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyPathConnectedSpace X] [LocallyPathConnectedSpace Y] :

LocallyPathConnectedSpace (X ⊕ Y)

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

@[deprecated Sum.locallyPathConnectedSpace (since := "2026-06-21")]

theorem Sum.locPathConnectedSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyPathConnectedSpace X] [LocallyPathConnectedSpace Y] :

LocallyPathConnectedSpace (X ⊕ Y)

Alias of Sum.locallyPathConnectedSpace.

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

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

LocallyPathConnectedSpace ((i : ι) × X i)

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

@[deprecated Sigma.locallyPathConnectedSpace (since := "2026-06-21")]

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

LocallyPathConnectedSpace ((i : ι) × X i)

Alias of Sigma.locallyPathConnectedSpace.

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

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

LocallyPathConnectedSpace X

@[deprecated AlexandrovDiscrete.locallyPathConnectedSpace (since := "2026-06-21")]

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

LocallyPathConnectedSpace X

Alias of AlexandrovDiscrete.locallyPathConnectedSpace.

instance instDiscreteTopologyZerothHomotopy {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] :

DiscreteTopology (ZerothHomotopy X)

If a space is locally path-connected, the topology of its path components is discrete.

instance instFiniteZerothHomotopyOfCompactSpace {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [CompactSpace X] :

Finite (ZerothHomotopy X)

A locally path-connected compact space has finitely many path components.