no goals
α : Type u
β : Type v
ι : Type ?u.71334
π : ι → Type ?u.71339
inst✝ : TopologicalSpace α
s✝ t u v s : Set α
h : IsPreconnected s
⊢ IsPreconnected univ
rwa [← inducing_subtype_val.isPreconnected_image, image_univ, Subtype.range_val]