instSuccOrder — Mathlib

English

The successor operation defined in the order structure on ℤ coincides with the standard successor function.

Русский

Операция следующего элемента в структуре порядка на ℤ совпадает с обычной функцией следующего элемента.

LaTeX

$$$\mathrm{Order.succ} = \mathrm{succ}$$$

Lean4

@[instance]
abbrev instSuccOrder : SuccOrder ℤ :=
  { SuccOrder.ofSuccLeIff succ fun {_ _} => Iff.rfl with succ := succ }

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