Minimal, Maximal, Least, and Greatest Elements w.r.t. Restricted Ordering

Martin Desharnais 📧

October 24, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This entry provides small, reusable, theories that specify the concepts of minimal, maximal, least, and greatest elements in sets, final sets, and final multisets. The concepts are uniformly specified as predicates parametrized by a binary relation. The binary relation is only required to be an ordering on the elements of the concrete collection considered. This is useful when working with a partial ordering, but some assumption or invariant proves that the ordering is total on all elements of the considered set.

License

BSD License

Topics

Session Min_Max_Least_Greatest