Theorems · Theorem · general topology

subsingleton_of_disjoint_isOpen_iUnion_eq_univ

∀ {α : Type u} {ι : Type u_1} [inst : TopologicalSpace α] [PreconnectedSpace α] {s : ι → Set α},
  (∀ (i : ι), (s i).Nonempty) →
    Pairwise (Function.onFun Disjoint s) → (∀ (i : ι), IsOpen (s i)) → ⋃ i, s i = Set.univ → Subsingleton ι

In a preconnected space, any disjoint cover by non-empty open subsets has at most one element.

Defined in

Mathlib.Topology.Connected.Clopen

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePreconnectedSpace