Theorems · Definition · general topology

ConnectedComponents.equivOfIsClopenOfIsConnected

{α : Type u} →
  [inst : TopologicalSpace α] →
    {ι : Type u_3} →
      {U : ι → Set α} →
        (∀ (i : ι), IsClopen (U i)) →
          Pairwise (Function.onFun Disjoint U) →
            ⋃ i, U i = Set.univ → (∀ (i : ι), IsConnected (U i)) → ConnectedComponents α ≃ ι

If ι indexes a disjoint union decomposition of α, it is equivalent to the connected components of α.

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

TopologicalSpace