Theorems · Theorem · general topology

ConnectedComponents.exists_fun_isClopen_of_infinite

∀ (α : Type u) [inst : TopologicalSpace α] [Infinite (ConnectedComponents α)] (n : ℕ),
  0 < n →
    ∃ U,
      (∀ (i : Fin n), IsClopen (U i)) ∧
        (∀ (i : Fin n), (U i).Nonempty) ∧ Pairwise (Function.onFun Disjoint U) ∧ ⋃ i, U i = Set.univ

If X has infinitely many connected components, it admits disjoint union decompositions with arbitrarily many summands.

Defined in

Mathlib.Topology.Connected.Clopen

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceInfinite