add — Mathlib

English

Define i + k : Fin2 (n + k) for i ∈ Fin2 n by recursion: i + 0 = i and i + (k+1) = fs (i + k).

Русский

Задать сложение i + k для i ∈ Fin2 n: i + 0 = i, и i + (k+1) = fs (i + k).

LaTeX

$$$\text{def }\mathrm{add}\{n\}(i: \mathrm{Fin2}\,n) : \forall k, \mathrm{Fin2}(n+k)\;\begin{cases} 0 & \text{when } i = 0 \\ \mathrm{fs}(\mathrm{add}\ i\ k) & \text{otherwise} \end{cases}$$$

Lean4

/-- `i + k : Fin2 (n + k)` when `i : Fin2 n` and `k : ℕ` -/
def add {n} (i : Fin2 n) : ∀ k, Fin2 (n + k)
  | 0 => i
  | succ k => fs (add i k)

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