sign_signedInfDist_incenter

Mathlib.Geometry.Euclidean.Incenter

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

← MathLib Explorer

English

The sign of the signedInfDist from the incenter to any face is 1.

Русский

Знак подписи расстояния между инцентром и гранями равен 1.

LaTeX

$$SignType.sign(s.signedInfDist i s.incenter) = 1$$

Lean4

theorem sign_signedInfDist_incenter (i : Fin (n + 1)) : SignType.sign (s.signedInfDist i s.incenter) = 1 :=
  by
  convert s.excenterExists_empty.sign_signedInfDist_excenter i
  simp

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

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

Разделы

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

Аффилиация

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