no goals
α : Type u
β : Type v
ι : Type ?u.140029
π : ι → Type ?u.140034
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
inst✝ : TotallyDisconnectedSpace β
f : α → β
h : Continuous f
⊢ ∀ (a b : α), Setoid.r a b → f a = f b
convert h.image_eq_of_connectedComponent_eq