Theorems · Definition · order theory

IsMax

{α : Type u_1} → [LE α] → α → Prop

a is a maximal element of α if no element is strictly greater than it. We spell it without < to avoid having to convert between ≤ and <. Instead, isMax_iff_forall_not_lt does the conversion.

Defined in

Mathlib.Order.Max

Cited by

372 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 3 definitions · uses no axioms

Assumes

LE