Upper and lower sets in a locally finite order #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we characterise the interaction of upper_set/lower_set and locally_finite_order.
@[protected]
theorem
set.finite.upper_closure
{α : Type u_1}
[preorder α]
{s : set α}
[locally_finite_order_top α]
(hs : s.finite) :
↑(upper_closure s).finite
@[protected]
theorem
set.finite.lower_closure
{α : Type u_1}
[preorder α]
{s : set α}
[locally_finite_order_bot α]
(hs : s.finite) :
↑(lower_closure s).finite