Topic: maximal/minimal elements
Floris van Doorn (May 16 2019 at 22:20):
Does the definition of maximal/minimal elements in a preorder exist in mathlib?
order.bounds least/greatest elements are defined, but I cannot find maximal/minimal elements.
x is a maximal element of a set
x is in
s and no
y > x.
Floris van Doorn (May 16 2019 at 22:21):
This definition could also be used to define
Last updated: May 13 2021 at 21:12 UTC