English
Pred is the predecessor operator in a Preorder with a PredOrder: pred a is the greatest element less than a if one exists, and pred a = a if a is minimal.
Русский
Pred — оператор предшественника в предпорядке: pred(a) — наибольший элемент, меньший чем a, если он существует; иначе pred(a) = a для минимальных элементов.
LaTeX
$$$ \text{pred} : \alpha \to \alpha, \quad \text{pred is the predecessor operator with } pred(a) < a \text{ when possible, and } pred(a)=a \text{ if } a \text{ is minimal}. $$$
Lean4
/-- The predecessor of an element. If `a` is not minimal, then `pred a` is the greatest element less
than `a`. If `a` is minimal, then `pred a = a`. -/
def pred : α → α :=
PredOrder.pred
