maximal/minimal elements

Stream: general

[Floris van Doorn]

Does the definition of maximal/minimal elements in a preorder exist in mathlib?
In order.bounds least/greatest elements are defined, but I cannot find maximal/minimal elements.
Recall that x is a maximal element of a set s if x is in s and no y in s satisfies y > x.

[Floris van Doorn]

This definition could also be used to define ideal.is_maximal