no goals
α : Type u_1
β : Type ?u.163100
γ : Type ?u.163103
ι : Sort ?u.163106
κ : ι → Sort ?u.163111
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
x : α
S : Set (Set α)
⊢ lowerClosure (⋃₀ S) = ⨆ (s : Set α) (_ : s ∈ S), lowerClosure s
simp_rw [sUnion_eq_biUnion, lowerClosure_iUnion]