Theorems · Theorem · general topology

IsConnected.iUnion_of_chain

∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] [inst_2 : SuccOrder β]
  [IsSuccArchimedean β] [Nonempty β] {s : β → Set α},
  (∀ (n : β), IsConnected (s n)) → (∀ (n : β), (s n ∩ s (Order.succ n)).Nonempty) → IsConnected (⋃ 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 connected.

Defined in

Mathlib.Topology.Connected.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderSuccOrderIsSuccArchimedeanNonempty