## Stream: general

### 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?
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 (May 16 2019 at 22:21):

This definition could also be used to define ideal.is_maximal

Last updated: May 13 2021 at 21:12 UTC