abs — Mathlib

English

The abstraction function abs for the projection QPF takes a representation in P i α to the actual i-th coordinate projection by evaluating the function component at the i-th index.

Русский

Функция абстракции abs для функторa проекции переводит представление в P_i α к фактической i-й координате проекции путём применения компонентной функции к индексу i.

LaTeX

$$$\\\\mathrm{abs}:\\\\Prj.P(i)\\\\;\\\\alpha \\\\to\\\\ Prj_i\\\\alpha\\\\;\\\\text{given by } \\\\mathrm{abs}(⟨x, f⟩) = f_i(x).$$$

Lean4

/-- Abstraction function of the `QPF` instance -/
def abs ⦃α : TypeVec n⦄ : Prj.P i α → Prj i α
  | ⟨_x, f⟩ => f _ ⟨⟨rfl⟩⟩

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