incenter_eq_affineCombination — Mathlib

English

The incenter of s is the affine combination of its vertices with weights given by the excenter weights for the empty sign set.

Русский

Инцентр s является аффинным сочетанием вершин с весами excenterWeights ∅.

LaTeX

$$s.incenter = Finset.univ.affineCombination ℝ s.points (s.excenterWeights ∅)$$

Lean4

theorem incenter_eq_affineCombination : s.incenter = Finset.univ.affineCombination ℝ s.points (s.excenterWeights ∅) :=
  rfl

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