Theorems · Theorem · general topology

ConnectedComponents.equivOfIsClopen_symm_mk

∀ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_3} {U : ι → Set α} (hclopen : ∀ (i : ι), IsClopen (U i))
  (hdisj : Pairwise (Function.onFun Disjoint U)) (hunion : ⋃ i, U i = Set.univ) {i : ι} (x : ↑(U i)),
  (ConnectedComponents.equivOfIsClopen hclopen hdisj hunion).symm ⟨i, ConnectedComponents.mk x⟩ =
    ConnectedComponents.mk ↑x

Defined in

Mathlib.Topology.Connected.Clopen

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace