α : Type u_1
β : Type ?u.4368
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
h : Set.Finite s
⊢ IsClosed (⋃ (i : α) (_ : i ∈ s), ↑(UpperSet.Ici i))
α : Type u_1
β : Type ?u.4368
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
h : Set.Finite s
⊢ IsClosed ↑(upperClosure s)
simp only [← UpperSet.iInf_Ici, UpperSet.coe_iInf]
no goals
α : Type u_1
β : Type ?u.4368
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
h : Set.Finite s
⊢ IsClosed (⋃ (i : α) (_ : i ∈ s), ↑(UpperSet.Ici i))
exact isClosed_biUnion h fun a _ => isClosed_Ici a