no goals
α✝ : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
a b : α✝
α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ ¬BddAbove s ↔ ∀ (x : α), ∃ y, y ∈ s ∧ x < y
simp only [not_bddAbove_iff', not_le]