Theorems · Theorem · general topology

Sigma.isPreconnected_iff

∀ {ι : Type u_1} {X : ι → Type u_2} [hι : Nonempty ι] [inst : (i : ι) → TopologicalSpace (X i)]
  {s : Set ((i : ι) × X i)}, IsPreconnected s ↔ ∃ i t, IsPreconnected t ∧ s = Sigma.mk i '' t

Defined in

Mathlib.Topology.Connected.Clopen

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonemptyTopologicalSpace