excenter_eq_affineCombination — Mathlib

English

The excenter of a simplex with a given sign set equals the affine combination of the simplex's vertices with weights given by the excenter weights for that sign set.

Русский

Экцентер симплексa с заданным набором знаков равен аффинному сочетанию вершин симплексa с весами, заданными для этого набора знаков.

LaTeX

$$s.excenter(\text{signs}) = Finset.univ.affineCombination \mathbb{R} s.points (s.excenterWeights signs)$$

Lean4

theorem excenter_eq_affineCombination (signs : Finset (Fin (n + 1))) :
    s.excenter signs = Finset.univ.affineCombination ℝ s.points (s.excenterWeights signs) :=
  rfl

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