excenter_mem_affineSpan_range — Mathlib

English

The signed distance from the excenter to the plane of each face equals, up to sign, the reciprocal of the sum of unnormalized excenter weights.

Русский

Знакомая подпись расстояния между эксцентром и проекцией на плоскость каждой грани равна, с учётом знака, обратной сумме несормированных весов эксцентра по соответствующим граням.

LaTeX

$$s.signedInfDist i (s.excenter signs) = (if i ∈ signs then -1 else 1) * (\sum j, s.excenterWeightsUnnorm signs j)^{-1}$$

Lean4

theorem excenter_mem_affineSpan_range {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) :
    s.excenter signs ∈ affineSpan ℝ (Set.range s.points) :=
  affineCombination_mem_affineSpan h.sum_excenterWeights_eq_one _

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