English
For any natural numbers n, m, the map i ↦ i + n gives an order-embedding from Fin(m) into Fin(n + m); the left addition shifts indices by n while preserving order.
Русский
Для любых натуральных чисел n, m отображение i ↦ i + n задаёт упорядочивающее вложение Fin(m) в Fin(n + m); добавление слева смещает индексы без нарушения порядка.
LaTeX
$$$i \mapsto i + n\;:\; \mathrm{Fin}(m) \hookrightarrow_{\mathrm{ord}} \mathrm{Fin}(n+m).$$$
Lean4
/-- `Fin.natAdd` as an `OrderEmbedding`.
`natAddOrderEmb n i` adds `n` to `i` "on the left". -/
@[simps! apply toEmbedding]
def natAddOrderEmb (n) : Fin m ↪o Fin (n + m) :=
.ofStrictMono (natAdd n) (strictMono_natAdd n)
