pair — Mathlib

English

The pairing function Nat.pair is given by: pair(a,b) = if a < b then b^2 + a else a^2 + a + b.

Русский

Парная функция Nat.pair задаётся: pair(a,b) = если a < b, тогда b^2 + a, иначе a^2 + a + b.

LaTeX

$$$$ \mathrm{pair}(a,b) = \begin{cases} b^{2} + a, & a < b, \\ a^{2} + a + b, & \text{else}. \end{cases} $$$$

Lean4

/-- Pairing function for the natural numbers. -/
@[pp_nodot]
def pair (a b : ℕ) : ℕ :=
  if a < b then b * b + a else a * a + a + b

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