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