α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
E : Type u_1
inst✝ : OrderIsoClass E α β
e : E
⊢ OrdConnected (↑e '' univ)
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
E : Type u_1
inst✝ : OrderIsoClass E α β
e : E
⊢ OrdConnected (range ↑e)
simp_rw [← image_univ]
no goals
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
E : Type u_1
inst✝ : OrderIsoClass E α β
e : E
⊢ OrdConnected (↑e '' univ)
exact ordConnected_image (e : α ≃o β)