ConnectedComponents.lean

theorem bijective_clopen_preimage (f : X ⟶ Y)
    [(pullback f).IsEquivalence] :
    Function.Bijective (fun U : Clopens Y ↦
      (⟨f ⁻¹' (U : Set Y), U.isClopen.preimage f.continuous⟩ : Clopens X)) := by
  constructor
  · intro U V h
    obtain ⟨W, _, hW⟩ := existsUnique_clopen_preimage_of_pullback_isEquivalence f
      ⟨f ⁻¹' (U : Set Y), U.isClopen.preimage f.continuous⟩
    have hpre : f ⁻¹' (U : Set Y) = f ⁻¹' (V : Set Y) :=
      congrArg (fun A : Clopens X ↦ (A : Set X)) h
    exact (hW U rfl).trans (hW V hpre.symm).symm
  · intro U
    obtain ⟨V, hV, _⟩ := existsUnique_clopen_preimage_of_pullback_isEquivalence f U
    exact ⟨V, Clopens.ext hV⟩

theorem connectedSpace_iff_of_pullback_isEquivalence
    (f : X ⟶ Y) [(pullback f).IsEquivalence] :
    ConnectedSpace X ↔ ConnectedSpace Y

theorem connectedComponentsMap_isHomeomorph_of_pullback_isEquivalence
    [CompactSpace X] [QuasiSeparatedSpace X] [CompactSpace Y] [QuasiSeparatedSpace Y]
    (f : X ⟶ Y) [(pullback f).IsEquivalence] :
    IsHomeomorph f.continuous.connectedComponentsMap