[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : β
h : IsLUB (↑f '' s) x
⊢ ∀ {x y : α}, ↑f x ≤ ↑f y ↔ x ≤ y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : β
h : IsLUB s (↑(symm f) x)
⊢ ∀ {x y : β}, ↑(symm f) x ≤ ↑(symm f) y ↔ x ≤ y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : α
⊢ IsLUB (↑f '' s) (↑f x) ↔ IsLUB s x
[PROOFSTEP]
rw [isLUB_image, f.symm_apply_apply]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set β
x : α
⊢ IsLUB (↑f ⁻¹' s) x ↔ IsLUB s (↑f x)
[PROOFSTEP]
rw [← f.symm_symm, ← image_eq_preimage, isLUB_image]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set β
x : β
⊢ IsLUB (↑f ⁻¹' s) (↑(symm f) x) ↔ IsLUB s x
[PROOFSTEP]
rw [isLUB_preimage, f.apply_symm_apply]
