Email Gateway (Oct 30 2024 at 06:58): Email Gateway (Oct 30 2024 at 06:58):From: Dmitriy Traytel <traytel@di.ku.dk>
Dear all,
The AFP newly provides us with means to master minimal, maximal, least, and greatest elements (https://xkcd.com/965/), uniformly:
Minimal, Maximal, Least, and Greatest Elements w.r.t. Restricted Ordering
by Martin Desharnais
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.
https://www.isa-afp.org/entries/Min_Max_Least_Greatest.html
Enjoy!
Dmitriy
Last updated: Jan 04 2025 at 20:18 UTC