insphere

Mathlib.Geometry.Euclidean.Incenter

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

English

The center of the exsphere equals the excenter for the same signs.

Русский

Центр экс сферы равен экцентру для тех же знаков.

LaTeX

$$(s.exsphere signs).center = s.excenter signs$$

Lean4

/-- The insphere of a simplex. -/
def insphere : Sphere P :=
  s.exsphere ∅

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

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

Разделы

Аффилиация

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