natAdd_castLEEmb — Mathlib

English

If n ≤ m, there is an embedding Fin n ↪ Fin m given by i ↦ i + (m − n).

Русский

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

LaTeX

$$$\forall n m (hmn : n \le m),\; \mathrm{Fin} n \hookrightarrow \mathrm{Fin} m,\ i \mapsto i + (m - n)$$$

Lean4

/-- `Fin.natAdd_castLEEmb` as an `Embedding` from `Fin n` to `Fin m`, by appending the former
at the end of the latter.
`natAdd_castLEEmb hmn i` maps `i : Fin m` to `i + (m - n) : Fin n` by adding `m - n` to `i` -/
@[simps!]
def natAdd_castLEEmb (hmn : n ≤ m) : Fin n ↪ Fin m :=
  (addNatEmb (m - n)).trans (finCongr (by cutsat)).toEmbedding

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