pred_lt_top — Mathlib

English

In any linear order with a top element, the predecessor of any element is strictly less than the top element.

Русский

В линейном порядке с верхним элементом предшественник любого элемента строго меньше верхнего элемента.

LaTeX

$$$\operatorname{pred} a < \top$$$

Lean4

theorem pred_lt_top (a : α) : pred a < ⊤ :=
  (pred_mono le_top).trans_lt <| pred_lt_of_not_isMin not_isMin_top

Похожие утверждения