Upper and lower sets in a locally finite order

In this file we characterise the interaction of UpperSet/LowerSet and LocallyFiniteOrder.

theorem Set.Finite.upperClosure {α : Type u_1} [Preorder α] {s : Set α} [LocallyFiniteOrderTop α] (hs : s.Finite) : (↑(upperClosure s)).Finite

theorem Set.Finite.lowerClosure {α : Type u_1} [Preorder α] {s : Set α} [LocallyFiniteOrderBot α] (hs : s.Finite) : (↑(lowerClosure s)).Finite