exsphere_radius — Mathlib

English

The inverse height equals the sum of the inverse heights of the other vertices, scaled with inner products, as given by inv_height_eq_sum_mul_inv_dist.

Русский

Обратная высота выражается через сумму обратных высот остальных вершин с использованием скалярного произведения.

LaTeX

$$h_i^{-1} = \sum_{j \ne i} -\frac{\langle p_i - a_i, p_j - a_j \rangle}{h_i h_j} \cdot h_j^{-1}$$

Lean4

@[simp]
theorem exsphere_radius (signs : Finset (Fin (n + 1))) : (s.exsphere signs).radius = s.exradius signs :=
  rfl

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