Theorems · Theorem · general topology

IsPreconnected.iUnion_of_chain

∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] [inst_2 : SuccOrder β]
  [IsSuccArchimedean β] {s : β → Set α},
  (∀ (n : β), IsPreconnected (s n)) → (∀ (n : β), (s n ∩ s (Order.succ n)).Nonempty) → IsPreconnected (⋃ n, s n)

The iUnion of connected sets indexed by a type with an archimedean successor (like ℕ or ℤ) such that any two neighboring sets meet is preconnected.

Defined in

Mathlib.Topology.Connected.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderSuccOrderIsSuccArchimedean