revAtFun_invol

Mathlib.Algebra.Polynomial.Reverse

URI: https://scilib.ai/kg/mathlib#Polynomial.revAtFun_invol

English

For every N and i, revAtFun N i equals N − i when i ≤ N, and equals i otherwise.

Русский

Для каждого N и i выполняется revAtFun N i = N − i, если i ≤ N, иначе i.

LaTeX

$$$\\mathrm{revAtFun}(N,i)=\\begin{cases}N-i,& i\\le N, \\\\ i,& i>N.\\end{cases}$$$

Lean4

theorem revAtFun_invol {N i : ℕ} : revAtFun N (revAtFun N i) = i :=
  by
  unfold revAtFun
  grind

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

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

Разделы

Аффилиация

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