natAddEmb — Mathlib

English

There is an embedding Fin m → Fin(n + m) given by i ↦ i + n on the left.

Русский

Существует вложение Fin m → Fin(n+m), заданное i ↦ i + n слева.

LaTeX

$$$ \mathrm{natAddEmb}(n) : \mathrm{Fin}(m) \hookrightarrow \mathrm{Fin}(n+m)$ with $\mathrm{toFun}(i)=i+n$$$

Lean4

/-- `Fin.natAdd` as an `Embedding`, `natAddEmb n i` adds `n` to `i` "on the left". -/
@[simps! apply]
def natAddEmb (n) {m} : Fin m ↪ Fin (n + m) where
  toFun := natAdd n
  inj' a b := by simp [Fin.ext_iff]

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