Theorems · Theorem · manifolds

ChartedSpace.locallyPathConnectedSpace

∀ (H : Type u) (M : Type u_2) [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [ChartedSpace H M]
  [LocallyPathConnectedSpace H], LocallyPathConnectedSpace M

If a topological space M admits an atlas with locally path-connected charts, then M itself is locally path-connected.

Defined in

Mathlib.Geometry.Manifold.ChartedSpace

Cited by

1 results in Mathlib

Foundations

Depth 131 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceChartedSpaceLocallyPathConnectedSpace