mkOfSucc — Mathlib

English

For each n and each i in Fin n, there is a canonical morphism mkOfSucc(i): Δ^1 → Δ^n selecting the arrow i → i+1 in Fin(n+1).

Русский

Для каждого n и каждого i ∈ Fin n существует канонический морфизм mkOfSucc(i): Δ^1 → Δ^n, выбирающий ребро i → i+1 в Fin(n+1).

LaTeX

$$$\mathrm{mkOfSucc}\{n\}\ (i) : \Delta^1 \to \Delta^n$$$

Lean4

/-- The morphism `⦋1⦌ ⟶ ⦋n⦌` that picks out the arrow `i ⟶ i+1` in `Fin (n+1)`. -/
def mkOfSucc {n} (i : Fin n) : ⦋1⦌ ⟶ ⦋n⦌ :=
  SimplexCategory.mkHom
    { toFun := fun
        | 0 => i.castSucc
        | 1 => i.succ
      monotone' := fun
        | 0, 0, _ | 1, 1, _ => le_rfl
        | 0, 1, _ => Fin.castSucc_le_succ i }

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