instSuccAddOrder

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.instSuccAddOrder

English

The ENNat order is equipped with a successor operation such that succ(x) = x + 1.

Русский

У ENat задан такой порядок с операцией преемника: succ(x) = x + 1.

LaTeX

$$$$\\operatorname{succ}_{\\mathbb{N}_{\\infty}}(x) = x + 1 \\quad\\text{for all } x.$$$

Lean4

instance : SuccAddOrder ℕ∞ where succ_eq_add_one x := by cases x <;> simp [SuccOrder.succ]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru