excenterWeightsUnnorm_empty_apply

Mathlib.Geometry.Euclidean.Incenter

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

English

When the set of signs is empty, the excenter weight equals the reciprocal of vertex height at i.

Русский

Для пустого множества знаков вес эксенцера равен обратному высоте вершины i.

LaTeX

$$$s.excenterWeightsUnnorm(\emptyset)(i) = (s.height(i))^{-1}$$$

Lean4

@[simp]
theorem excenterWeightsUnnorm_empty_apply (i : Fin (n + 1)) : s.excenterWeightsUnnorm ∅ i = (s.height i)⁻¹ :=
  one_mul _

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

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

Разделы

Аффилиация

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