coord — Mathlib

English

Reindexed basis corresponds to the reindexed of the original basis of i.

Русский

Переиндексированный базис соответствует переиндексированному исходному базису i.

LaTeX

$$$(b.reindex e).basisOf i = (b.basisOf (e^{-1} i)).reindex (e.subtypeEquiv ...) $$$

Lean4

/-- The `i`th barycentric coordinate of a point. -/
noncomputable def coord (i : ι) : P →ᵃ[k] k
    where
  toFun q := 1 - (b.basisOf i).sumCoords (q -ᵥ b i)
  linear := -(b.basisOf i).sumCoords
  map_vadd' q
    v := by
    rw [vadd_vsub_assoc, LinearMap.map_add, vadd_eq_add, LinearMap.neg_apply, sub_add_eq_sub_sub_swap, add_comm,
      sub_eq_add_neg]

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