Theorems · Definition · order theory

IsMin

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

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

Defined in

Mathlib.Order.Max

Cited by

277 results in Mathlib

Foundations

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

Assumes

LE