case h.e'_3
α : Type u_1
β : Type ?u.1894
γ : Type ?u.1897
ι : Sort ?u.1900
κ : ι → Sort ?u.1905
inst✝¹ : LE α
inst✝ : LE β
s t : Set α
h : IsLowerSet (sᶜ)
⊢ s = sᶜᶜ
α : Type u_1
β : Type ?u.1894
γ : Type ?u.1897
ι : Sort ?u.1900
κ : ι → Sort ?u.1905
inst✝¹ : LE α
inst✝ : LE β
s t : Set α
h : IsLowerSet (sᶜ)
⊢ IsUpperSet s
convert h.compl
no goals
case h.e'_3
α : Type u_1
β : Type ?u.1894
γ : Type ?u.1897
ι : Sort ?u.1900
κ : ι → Sort ?u.1905
inst✝¹ : LE α
inst✝ : LE β
s t : Set α
h : IsLowerSet (sᶜ)
⊢ s = sᶜᶜ
rw [compl_compl]