Theorems · Theorem · general topology

Pi.locallyConnectedSpace_of_finite_not_preconnectedSpace

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

If each X i is locally connected and all but finitely many are preconnected, then ∀ i, X i is locally connected.

Defined in

Mathlib.Topology.Connected.LocallyConnected

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLocallyConnectedSpace