α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
E : Type u_1
inst✝ : OrderIsoClass E α β
e : E
s : Set α
hs : OrdConnected s
⊢ OrdConnected (↑(OrderIso.symm ↑e) ⁻¹' s)
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
E : Type u_1
inst✝ : OrderIsoClass E α β
e : E
s : Set α
hs : OrdConnected s
⊢ OrdConnected (↑e '' s)
erw [(e : α ≃o β).image_eq_preimage]
no goals
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
E : Type u_1
inst✝ : OrderIsoClass E α β
e : E
s : Set α
hs : OrdConnected s
⊢ OrdConnected (↑(OrderIso.symm ↑e) ⁻¹' s)
apply ordConnected_preimage (e : α ≃o β).symm