Theorems · Theorem · general topology

isPreconnected_iff_subset_of_disjoint_closed

∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
  IsPreconnected s ↔ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

A set s is preconnected if and only if for every cover by two closed sets that are disjoint on s, it is contained in one of the two covering sets.

Defined in

Mathlib.Topology.Connected.Clopen

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpace