Maximal elements of a partial order

Stream: Is there code for X?

[Thomas Browning]

Does mathlib have a name for maximal elements of a partial order (elements x satisfying x ≤ y → x = y)?

[Yaël Dillies]

We call them is_maximal, but I don't think there's a dedicated predicate. Of course, for top orders, the unique maximal element will be called top.

[Yaël Dillies]

You can also use upper_bound univ in total orders.

[Kevin Buzzard]

(deleted)

[Yaël Dillies]

Whoops sorry I meant linear_order

[Thomas Browning]

The case I have in mind are Sylow subgroups (maximal among p-subgroups), in which case top or upper_bound univ wouldn't work.

[Thomas Browning]

Yaël Dillies said:

We call them is_maximal, but I don't think there's a dedicated predicate. Of course, for top orders, the unique maximal element will be called top.

Are you saying that is_maximal is the naming convention, but there's no def is_maximal in mathlib?

[Yaël Dillies]

Exactly