Theorems · Theorem · general topology

Pi.locallyConnectedSpace_iff

∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)],
  LocallyConnectedSpace ((i : ι) → X i) ↔
    IsEmpty ((i : ι) → X i) ∨ (∀ (i : ι), LocallyConnectedSpace (X i)) ∧ {i | ¬PreconnectedSpace (X i)}.Finite

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

Defined in

Mathlib.Topology.Connected.LocallyConnected

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace