pointWeightsWithCircumcenter — Mathlib

English

The weights for a single vertex of a simplex with respect to pointsWithCircumcenter are 1 at that vertex and 0 otherwise, and 0 for the circumcenter index.

Русский

Вес вершины простого многогранника по отношению к pointsWithCircumcenter: единица на данной вершине, ноль для остальных и ноль для circumcenterIndex.

LaTeX

$$$\text{pointWeightsWithCircumcenter}(i)(j)=\begin{cases} 1 & \text{if } j=i \\ 0 & \text{otherwise} \end{cases};\text{ and } \text{pointWeightsWithCircumcenter}(i)(\text{circumcenterIndex})=0$$$

Lean4

/-- The weights for a single vertex of a simplex, in terms of
`pointsWithCircumcenter`. -/
def pointWeightsWithCircumcenter {n : ℕ} (i : Fin (n + 1)) : PointsWithCircumcenterIndex n → ℝ
  | pointIndex j => if j = i then 1 else 0
  | circumcenterIndex => 0

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