English
The coords map assigns to each point p ∈ P a function i ↦ coord_i(p), i.e., the barycentric coordinate function associated to p with respect to the basis b.
Русский
Координаты определяют отображение, которое каждой точке p ∈ P ставит в соответствующую функцию i ↦ coord_i(p).
LaTeX
$$$\\text{coords}: P \\to^{\\mathrm{aff}} (ι \\to k),\\; coords(p)(i) = b.coord\\, i\\; p$$$
Lean4
/-- Barycentric coordinates as an affine map. -/
noncomputable def coords : P →ᵃ[k] ι → k where
toFun q i := b.coord i q
linear :=
{ toFun := fun v i => -(b.basisOf i).sumCoords v
map_add' := fun v w => by ext; simp only [LinearMap.map_add, Pi.add_apply, neg_add]
map_smul' := fun t v => by ext; simp }
map_vadd' p v := by ext; simp
