ofNatSucc

Mathlib.Data.Num.Basic

URI: https://scilib.ai/kg/mathlib#PosNum.ofNatSucc

English

There is an instance that provides OfNat PosNum (n+1) with ofNat := ofNat (n+1).

Русский

Существует инстанс, задающий OfNat PosNum (n+1) через ofNat (n+1).

LaTeX

$$instance (priority := low) {n : ℕ} : OfNat PosNum (n + 1) where ofNat := ofNat (n + 1)$$

Lean4

/-- `ofNatSucc n` is the `PosNum` corresponding to `n + 1`. -/
def ofNatSucc : ℕ → PosNum
  | 0 => 1
  | Nat.succ n => succ (ofNatSucc n)

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

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

Разделы

Аффилиация

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