α : Type u_1
β : Type u_2
γ : Type ?u.18624
ι : Sort ?u.18627
κ : ι → Sort ?u.18632
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
p : α → Prop
a : α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet (↑↑f '' s)
α : Type u_1
β : Type u_2
γ : Type ?u.18624
ι : Sort ?u.18627
κ : ι → Sort ?u.18632
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
p : α → Prop
a : α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet (↑f '' s)
change IsUpperSet ((f : α ≃ β) '' s)
α : Type u_1
β : Type u_2
γ : Type ?u.18624
ι : Sort ?u.18627
κ : ι → Sort ?u.18632
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
p : α → Prop
a : α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet (↑(↑f).symm ⁻¹' s)
α : Type u_1
β : Type u_2
γ : Type ?u.18624
ι : Sort ?u.18627
κ : ι → Sort ?u.18632
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
p : α → Prop
a : α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet (↑↑f '' s)
rw [Set.image_equiv_eq_preimage_symm]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.18624
ι : Sort ?u.18627
κ : ι → Sort ?u.18632
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
p : α → Prop
a : α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet (↑(↑f).symm ⁻¹' s)
exact hs.preimage f.symm.monotone