revAtFun — Mathlib

English

For every N, the map i ↦ revAtFun N i is an involution on the natural numbers, i.e., applying it twice returns the original index: revAtFun N (revAtFun N i) = i.

Русский

Для каждого N отображение i ↦ revAtFun N i является инволюцией на естественных числах: повторное применение возвращает исходное значение: revAtFun N (revAtFun N i) = i.

LaTeX

$$$\\forall N,i \\in \\mathbb{N},\\; \\mathrm{revAtFun}(N,\\mathrm{revAtFun}(N,i)) = i.$$$

Lean4

/-- If `i ≤ N`, then `revAtFun N i` returns `N - i`, otherwise it returns `i`.
This is the map used by the embedding `revAt`.
-/
def revAtFun (N i : ℕ) : ℕ :=
  ite (i ≤ N) (N - i) i

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