le_pred_iff_eq_bot — Mathlib

English

In any order with a bottom element and predecessor, a ≤ pred(a) holds if and only if a is the bottom element.

Русский

В порядке с нижней гранью и предшественником для любого элемента a верно: a ≤ pred(a) тогда и только тогда, когда a = ⊥.

LaTeX

$$$a \le \operatorname{pred} a \iff a = \bot$$$

Lean4

theorem le_pred_iff_eq_bot : a ≤ pred a ↔ a = ⊥ :=
  @succ_le_iff_eq_top αᵒᵈ _ _ _ _

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