no goals
α : Type u_1
β : Type ?u.30000
γ : Type ?u.30003
ι : Sort ?u.30006
κ : ι → Sort ?u.30011
inst✝ : PartialOrder α
s : Set α
⊢ IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Ioi a ⊆ s
simp [isUpperSet_iff_forall_lt, subset_def, @forall_swap (_ ∈ s)]