α : Type u_1
β : Type u_2
γ : Type ?u.131603
ι : Sort ?u.131606
κ : ι → Sort ?u.131611
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
x : α
f : α ≃o β
⊢ upperClosure (↑f '' s) = ↑(OrderIso.symm (UpperSet.map (OrderIso.symm f))) (upperClosure s)
α : Type u_1
β : Type u_2
γ : Type ?u.131603
ι : Sort ?u.131606
κ : ι → Sort ?u.131611
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
x : α
f : α ≃o β
⊢ upperClosure (↑f '' s) = ↑(UpperSet.map f) (upperClosure s)
rw [← f.symm_symm, ← UpperSet.symm_map, f.symm_symm]
case a.h
α : Type u_1
β : Type u_2
γ : Type ?u.131603
ι : Sort ?u.131606
κ : ι → Sort ?u.131611
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
x : α
f : α ≃o β
x✝ : β
⊢ x✝ ∈ ↑(upperClosure (↑f '' s)) ↔ x✝ ∈ ↑(↑(OrderIso.symm (UpperSet.map (OrderIso.symm f))) (upperClosure s))
α : Type u_1
β : Type u_2
γ : Type ?u.131603
ι : Sort ?u.131606
κ : ι → Sort ?u.131611
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
x : α
f : α ≃o β
⊢ upperClosure (↑f '' s) = ↑(OrderIso.symm (UpperSet.map (OrderIso.symm f))) (upperClosure s)
ext
no goals
case a.h
α : Type u_1
β : Type u_2
γ : Type ?u.131603
ι : Sort ?u.131606
κ : ι → Sort ?u.131611
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
x : α
f : α ≃o β
x✝ : β
⊢ x✝ ∈ ↑(upperClosure (↑f '' s)) ↔ x✝ ∈ ↑(↑(OrderIso.symm (UpperSet.map (OrderIso.symm f))) (upperClosure s))
simp [-UpperSet.symm_map, UpperSet.map, OrderIso.symm, ← f.le_symm_apply]