instSuccAddOrder — Mathlib

English

There exists a canonical SuccAddOrder structure on ℕ, giving a compatible interaction between the successor operation and addition.

Русский

Натуральные числа наделены каноническим структурным порядком SuccAddOrder, обеспечивающим совместимость операции successor и сложения.

LaTeX

$$$\\text{There exists a canonical }\\mathrm{SuccAddOrder}(\\mathbb N).$$$

Lean4

instance instSuccAddOrder : SuccAddOrder ℕ :=
  ⟨fun _ => rfl⟩
    -- so that Lean reads `Nat.pred` through `pred_order.pred`

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