proj — Mathlib

English

Evaluation at index i acts as a projection: the ith component of the affine map proj i(f) equals f(i) when f is viewed as a function with i-th coordinate.

Русский

Оценка по индексу i действует как проекция: i-я компонента proj i(f) равна f(i).

LaTeX

$$$ (\\text{proj } i)\\, f = f(i) $$$

Lean4

/-- Evaluation at a point as an affine map. -/
def proj (i : ι) : (∀ i : ι, P i) →ᵃ[k] P i where
  toFun f := f i
  linear := @LinearMap.proj k ι _ V _ _ i
  map_vadd' _ _ := rfl

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