α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderBot α
hs : Set.Finite s
⊢ Set.Finite (⋃ (a : α) (_ : a ∈ s), Iic a)
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderBot α
hs : Set.Finite s
⊢ Set.Finite ↑(lowerClosure s)
rw [coe_lowerClosure]
no goals
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderBot α
hs : Set.Finite s
⊢ Set.Finite (⋃ (a : α) (_ : a ∈ s), Iic a)
exact hs.biUnion fun _ _ => finite_Iic _