[GOAL]
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderTop α
hs : Set.Finite s
⊢ Set.Finite ↑(upperClosure s)
[PROOFSTEP]
rw [coe_upperClosure]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderTop α
hs : Set.Finite s
⊢ Set.Finite (⋃ (a : α) (_ : a ∈ s), Ici a)
[PROOFSTEP]
exact hs.biUnion fun _ _ => finite_Ici _
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderBot α
hs : Set.Finite s
⊢ Set.Finite ↑(lowerClosure s)
[PROOFSTEP]
rw [coe_lowerClosure]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderBot α
hs : Set.Finite s
⊢ Set.Finite (⋃ (a : α) (_ : a ∈ s), Iic a)
[PROOFSTEP]
exact hs.biUnion fun _ _ => finite_Iic _
