id — Mathlib · SciLib

English

The identity arrow on α maps every component to itself, i.e., (TypeVec.id α) i (x) = x for all i and x ∈ α(i).

Русский

Идентичная стрелка на α переводит каждый компонент в себя: (TypeVec.id α) i (x) = x.

LaTeX

$$$ (\\text{TypeVec.id})(\\alpha) : \\alpha \\Rightarrow \\alpha $ with $ (\\text{TypeVec.id})(i)(x) = x $ for all i, x.$$

Lean4

/-- identity of arrow composition -/
def id {α : TypeVec n} : α ⟹ α := fun _ x => x

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