finRange_succ_eq_map — Mathlib

English

The finite range satisfies a simple recurrence: finRange(n+1) = 0 :: (finRange n).map Fin.succ.

Русский

Для конечного диапазона выполняется рекуррентное выражение: finRange(n+1) = 0 :: (finRange n).map Fin.succ.

LaTeX

$$$$ \\text{finRange}(n+1) = 0 \\;::\\; (\\text{finRange}(n)).\\text{map } Fin.succ. $$$$

Lean4

theorem finRange_succ_eq_map (n : ℕ) : finRange n.succ = 0 :: (finRange n).map Fin.succ :=
  finRange_succ

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