inradius_eq_abs_inv_sum — Mathlib

English

The inradius of s equals the absolute value of the inverse of the sum of the empty excenter weights unnormalized.

Русский

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

LaTeX

$$s.inradius = \left|\left(\sum_i s.excenterWeightsUnnorm ∅ i\right)^{-1}\right|$$

Lean4

theorem inradius_eq_abs_inv_sum : s.inradius = |(∑ i, s.excenterWeightsUnnorm ∅ i)⁻¹| :=
  rfl

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