castSucc — Mathlib

English

castSucc embeds Fin2 n into Fin2 (n+1) by keeping fz fixed and recursing on successors.

Русский

castSucc встраивает Fin2 n в Fin2 (n+1): fz остаётся, а fs применяем по рекурсии.

LaTeX

$$$\text{castSucc} : \forall n,\ Fin2 n \to Fin2 (n+1),\; \text{castSucc}(\mathrm{fz}) = \mathrm{fz},\; \text{castSucc}(\mathrm{fs} k) = \mathrm{fs}(\text{castSucc } k)$$$

Lean4

/-- `castSucc i` embeds `i : Fin2 n` in `Fin2 (n+1)`. -/
def castSucc {n} : Fin2 n → Fin2 (n + 1)
  | fz => fz
  | fs k => fs <| castSucc k

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