English
Let m ∈ N. The map i ↦ i + m defines an order-preserving embedding from Fin(n) into Fin(n + m); in particular i < j implies i + m < j + m, so the indices are shifted by m without disturbing the order.
Русский
Пусть m ∈ N. Отображение i ↦ i + m задаёт порядок-сохраняющее вложение Fin(n) в Fin(n + m); следовательно, если i < j, то i + m < j + m, то есть порядок сохраняется после прибавления m.
LaTeX
$$$i \mapsto i + m$ defines an order-embedding $\mathrm{Fin}(n) \hookrightarrow_{\mathrm{ord}} \mathrm{Fin}(n+m)$ and is strictly increasing: $i < j \implies i + m < j + m$.$$
Lean4
/-- `Fin.addNat` as an `OrderEmbedding`.
`addNatOrderEmb m i` adds `m` to `i`, generalizes `Fin.succ`. -/
@[simps! apply toEmbedding]
def addNatOrderEmb (m) : Fin n ↪o Fin (n + m) :=
.ofStrictMono (addNat · m) (strictMono_addNat m)
