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 : Set.Finite s)
:
Set.Finite ↑(upperClosure s)
theorem
Set.Finite.lowerClosure
{α : Type u_1}
[Preorder α]
{s : Set α}
[LocallyFiniteOrderBot α]
(hs : Set.Finite s)
:
Set.Finite ↑(lowerClosure s)