succ_one — Mathlib

English

For any α with a preorder, an OrderBot, an AddMonoidWithOne, and SuccAddOrder, succ_natCast(n) states that the successor of n embedded in WithBot α equals n+1.

Русский

Для любого α с предorder, OrderBot, AddMonoidWithOne и SuccAddOrder, succ_natCast(n) говорит, что переход в WithBot α числа n даёт n+1.

LaTeX

$$$$\operatorname{succ}(n) = n + 1 \quad \text{in } \mathrm{WithBot} \ \alpha$$$$

Lean4

@[simp]
theorem succ_one : succ (1 : WithBot α) = 2 := by simpa [one_add_one_eq_two] using succ_natCast 1

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