addNatEmb — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- `Fin.addNat` as an `Embedding`, `addNatEmb m i` adds `m` to `i`, generalizes `Fin.succ`. -/
@[simps! apply]
def addNatEmb (m) : Fin n ↪ Fin (n + m) where
  toFun := (addNat · m)
  inj' a b := by simp [Fin.ext_iff]

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