Zulip Chat Archive

Stream: general

Topic: maximal/minimal elements


view this post on Zulip 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.

view this post on Zulip 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