succ_coe — Mathlib

English

For any a in α, the successor of its embedding in WithBot α coincides with the order-theoretic successor of a: succ(a : WithBot α) = Order.succ a.

Русский

Для любого a из α переход к следующему элементу после его внедрения в WithBot α совпадает с порядковым переходом: succ(a : WithBot α) = Order.succ a.

LaTeX

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

Lean4

/-- Not to be confused with `WithBot.orderSucc_coe`, which is about `Order.succ`. -/
@[simp]
theorem succ_coe (a : α) : succ (a : WithBot α) = Order.succ a :=
  rfl

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