exradius_eq_abs_inv_sum — Mathlib

English

The exradius with respect to a sign set equals the absolute value of the inverse of the sum of the corresponding unnormalized excenter weights.

Русский

Эксрадиус по набору знаков равен модулю обратной суммы соответствующих не нормированных весов эксцентрa.

LaTeX

$$s.exradius(\text{signs}) = \left|\left(\sum_j s.excenterWeightsUnnorm signs j\right)^{-1}\right|$$

Lean4

theorem exradius_eq_abs_inv_sum (signs : Finset (Fin (n + 1))) :
    s.exradius signs = |(∑ i, s.excenterWeightsUnnorm signs i)⁻¹| :=
  rfl

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