diag — Mathlib

English

For every n, there is a canonical morphism diag(n): Δ^1 → Δ^n which picks out the diagonal edge from the first vertex to the last vertex of Δ^n.

Русский

Для каждого n существует канонический морфизм diag(n): Δ^1 → Δ^n, который выбирает диагональный ребро от вершины 0 до вершины n в Δ^n.

LaTeX

$$$\mathrm{diag}(n) = \mathrm{mkOfLe}(0,\mathrm{Fin.last}(n))$$$

Lean4

/-- The morphism `⦋1⦌ ⟶ ⦋n⦌` that picks out the "diagonal composite" edge -/
def diag (n : ℕ) : ⦋1⦌ ⟶ ⦋n⦌ :=
  mkOfLe 0 (Fin.last n) (Fin.zero_le _)

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