succ₂

Mathlib.Data.PNat.Xgcd

URI: https://scilib.ai/kg/mathlib#PNat.XgcdType.succ₂

English

succ₂ acts on a pair by incrementing both components by one: succ₂(t) = (t.1 + 1, t.2 + 1).

Русский

succ₂ действует на пару, увеличивая обе компоненты на единицу: succ₂(t) = (t.1 + 1, t.2 + 1).

LaTeX

$$$succ\\_2(t) = (t\\_1 + 1, t\\_2 + 1)$$$

Lean4

/-- `succ₂ [t.1, t.2] = [t.1.succ, t.2.succ]` -/
def succ₂ (t : ℕ × ℕ) : ℕ × ℕ :=
  ⟨t.1.succ, t.2.succ⟩

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

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

Разделы

Аффилиация

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