castAddEmb — Mathlib

English

There is an embedding castAddEmb m : Fin n ↪ Fin (n + m) given by i ↦ i + m.

Русский

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

LaTeX

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

Lean4

/-- `Fin.castAdd` as an `Embedding`, `castAddEmb m i` embeds `i : Fin n` in `Fin (n+m)`.
See also `Fin.natAddEmb` and `Fin.addNatEmb`. -/
def castAddEmb (m) : Fin n ↪ Fin (n + m) :=
  castLEEmb (le_add_right n m)

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