Theorems · Theorem · general topology

Pi.locallyPathConnectedSpace_iff

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

A product of spaces is locally path-connected iff it is empty, or every factor is locally path-connected and all but finitely many factors are path-connected.

Defined in

Mathlib.Topology.Connected.LocallyPathConnected

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace