α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : NoMinOrder α
hs : IsLUB s a
a' : α
ha' : a' < a
h : s = ∅
⊢ a' ∈ univ
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : NoMinOrder α
hs : IsLUB s a
a' : α
ha' : a' < a
h : s = ∅
⊢ a' ∈ upperBounds s
rw [h, upperBounds_empty]
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : NoMinOrder α
hs : IsLUB s a
a' : α
ha' : a' < a
h : s = ∅
⊢ a' ∈ univ
exact mem_univ _