exradius

Mathlib.Geometry.Euclidean.Incenter

URI: https://scilib.ai/kg/mathlib#Affine.Simplex.exradius

← MathLib Explorer

English

The exradius is the radius of the exsphere corresponding to signs.

Русский

Радиус экс сферы соответствует знакам.

LaTeX

$$exradius(signs) = (s.exsphere signs).radius$$

Lean4

/-- The distance between an excenter and a face of the simplex (zero if no such excenter
exists). -/
def exradius (signs : Finset (Fin (n + 1))) : ℝ :=
  (s.exsphere signs).radius

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru