Documentation

Mathlib.Order.UpperLower.LocallyFinite

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