pred_lt_iff_ne_bot — Mathlib

English

For any a in a pred-order with a bottom, pred(a) < a if and only if a is not the bottom element.

Русский

Для любого a в порядке с предшественником и нулём предшественник a меньше a тогда и только тогда, когда a не является низшей гранью.

LaTeX

$$$\operatorname{pred} a < a \iff a \neq \bot$$$

Lean4

theorem pred_lt_iff_ne_bot : pred a < a ↔ a ≠ ⊥ :=
  @lt_succ_iff_ne_top αᵒᵈ _ _ _ _

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