Mathlib Map

Theorems · Theorem · general topology

LocallyPathConnectedSpace.path_connected_basis

∀ {X : Type u_4} {inst : TopologicalSpace X} [self : LocallyPathConnectedSpace X] (x : X),
  (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsPathConnected s) id

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

Defined in
Mathlib.Topology.Connected.LocallyPathConnected
Cited by
5 results in Mathlib
Foundations
Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
LocallyPathConnectedSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsOpen.pathComponentIn · cited by 5IsOpen.pathComponentInIsLocalHomeomorph.existsUnique_continuousMap_lifts · cited by 2IsLocalHomeomorph.existsU…IsClosed.pathComponent · cited by 1IsClosed.pathComponentpathConnected_subset_basis · cited by 1pathConnected_subset_basisLocPathConnectedSpace.path_connected_basis · cited by 0LocPathConnectedSpace.pat…Set · cited by 53352SetTopologicalSpace · cited by 24529TopologicalSpaceFilter · cited by 8121Filternhds · cited by 5554nhdsFilter.HasBasis · cited by 604Filter.HasBasisIsPathConnected · cited by 65IsPathConnectedLocallyPathConnectedSpace · cited by 53LocallyPathConnectedSpaceLocallyPathConnectedSpace.pat…CITED BYCITES

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by5

Results whose statement or proof uses this declaration.