succ_eq_succ — Mathlib

English

For every a ∈ WithBot α, succ a = Order.succ a; the successor agrees with the ambient order on α.

Русский

Для каждого a ∈ WithBot αsucc a = Order.succ a; переход к следующему элементу согласуется с упорядочением α.

LaTeX

$$$$ \forall a:\mathrm{WithBot}\,\alpha,\ \operatorname{succ} a = \mathrm{Order.succ} a $$$$

Lean4

theorem succ_eq_succ : ∀ a : WithBot α, succ a = Order.succ a
  | ⊥ => rfl
  | (a : α) => rfl

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