instSuccAddOrder — Mathlib

English

The integers admit a SuccAddOrder structure, i.e., a compatible combination of successor and addition order properties (defined so that predecessor is read via PredOrder).

Русский

Целые числа обладают структурой SuccAddOrder, т.е. согласованностью между операцией следующего элемента и порядком сложения на Z (определено так, чтобы предшественник считывался через PredOrder).

LaTeX

$$$\text{SuccAddOrder}(\mathbb{Z})$$$

Lean4

instance instSuccAddOrder : SuccAddOrder ℤ :=
  ⟨fun _ => rfl⟩
    -- so that Lean reads `Int.pred` through `PredOrder.pred`

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