Theorems · Theorem · general topology

Pi.locallyPathConnectedSpace_of_finite_not_pathConnectedSpace

∀ {ι : Type u_3} {Z : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (Z i)]
  [∀ (i : ι), LocallyPathConnectedSpace (Z i)],
  {i | ¬PathConnectedSpace (Z i)}.Finite → LocallyPathConnectedSpace ((i : ι) → Z i)

If each Z i is locally path-connected and all but finitely many are path-connected, then ∀ i, Z i is locally path-connected.

Defined in

Mathlib.Topology.Connected.LocallyPathConnected

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLocallyPathConnectedSpace