hom_succ — Mathlib

English

In the category Fin n, for each i, there is a canonical morphism i.castSucc → i.succ, arising from the order embedding.

Русский

В категории Fin n для каждого элемента i существует каноническая стрелка i.castSucc → i.succ, возникающая из порядка вложения.

LaTeX

$$$\mathrm{hom}_{\mathrm{Fin}(n)}(i^{\mathrm{castSucc}}, i^{\mathrm{succ}}) = \mathrm{homOfLE}(\mathrm{Fin.castSucc\le\succ}(i)).$$$

Lean4

/-- The generating arrow `i ⟶ i+1` in the category `Fin n` -/
def hom_succ {n} (i : Fin n) : i.castSucc ⟶ i.succ :=
  homOfLE (Fin.castSucc_le_succ i)

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