natPred

Mathlib.Data.PNat.Defs

URI: https://scilib.ai/kg/mathlib#PNat.natPred

English

Predecessor of a ℕ⁺ element is its predecessor as a natural number.

Русский

Предшественник элемента ℕ⁺ — это его предшественник по отношению к натуральному числу.

LaTeX

$$$ \\forall i \\in \\mathbb{N}^+,\\; \\operatorname{natPred}(i) = i - 1.$$$$

Lean4

/-- Predecessor of a `ℕ+`, as a `ℕ`. -/
def natPred (i : ℕ+) : ℕ :=
  i - 1

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

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

Разделы

Аффилиация

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