English
revAt N defines an embedding of natural numbers into natural numbers, given by toFun i = if i ≤ N then N − i else i, and it is used as an embedding revAt.
Русский
revAt N задает вложение ℕ в ℕ, определяемое как toFun i = если i ≤ N тогда N − i иначе i, и используется как вложение revAt.
LaTeX
$$$\\text{revAt}(N)(i)=\\begin{cases}N-i,& i\\le N \\\\ i,& i>N.\\end{cases}$$$
Lean4
/-- If `i ≤ N`, then `revAt N i` returns `N - i`, otherwise it returns `i`.
Essentially, this embedding is only used for `i ≤ N`.
The advantage of `revAt N i` over `N - i` is that `revAt` is an involution.
-/
def revAt (N : ℕ) : Function.Embedding ℕ ℕ
where
toFun i := ite (i ≤ N) (N - i) i
inj' := revAtFun_inj
