excenterExists_singleton — Mathlib

English

The exsphere is defined as the sphere with center at the excenter and radius equal to the reciprocal of the sum of unnormalized excenter weights.

Русский

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

LaTeX

$$exsphere(signs) : center = s.excenter signs, radius = |(\sum_i s.excenterWeightsUnnorm signs i)^{-1}|$$

Lean4

/-- The existence of the excenter opposite a vertex (in two or more dimensions), expressed in
terms of `ExcenterExists`. -/
theorem excenterExists_singleton [Nat.AtLeastTwo n] (i : Fin (n + 1)) : s.ExcenterExists { i } :=
  (s.sum_excenterWeightsUnnorm_singleton_pos i).ne'

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