succEmb — Mathlib

English

For any n and m, there is an embedding Fin n → Fin (n + m) given by casting with addition: i ↦ i with an added m.

Русский

Для любых n, m существует вложение Fin n → Fin (n + m), задаваемое добавлением m: i ↦ i + m.

LaTeX

$$$ f(i) = \mathrm{castLE}(i, m) = i + m \quad \text{defines an embedding } Fin(n) \hookrightarrow Fin(n+m)$$

Lean4

/-- `Fin.succ` as an `Embedding` -/
def succEmb (n : ℕ) : Fin n ↪ Fin (n + 1) where
  toFun := succ
  inj' := succ_injective _

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