no goals
α : Type u
β : Type v
ι : Type ?u.72105
π : ι → Type ?u.72110
inst✝ : TopologicalSpace α
s✝ t u v s : Set α
h : PreconnectedSpace ↑s
⊢ IsPreconnected s
simpa using isPreconnected_univ.image ((↑) : s → α) continuous_subtype_val.continuousOn