no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
a b : α
⊢ upperBounds ∅ = univ
simp only [upperBounds, eq_univ_iff_forall, mem_setOf_eq, ball_empty_iff, forall_true_iff]