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