no goals
α : Type u_1
β : Type ?u.166274
γ : Type ?u.166277
ι : Sort ?u.166280
κ : ι → Sort ?u.166285
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
x : α
⊢ BddBelow ↑(upperClosure s) ↔ BddBelow s
simp_rw [BddBelow, lowerBounds_upperClosure]