exradius_singleton_pos

Mathlib.Geometry.Euclidean.Incenter

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

English

For any index i, the exradius of s with respect to the singleton {i} is positive.

Русский

Для любого индекса i эксрадиус s по одиночному множеству {i} положителен.

LaTeX

$$0 < s.exradius {i}$$

Lean4

theorem exradius_singleton_pos [Nat.AtLeastTwo n] (i : Fin (n + 1)) : 0 < s.exradius { i } :=
  (s.excenterExists_singleton i).exradius_pos

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

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

Разделы

Аффилиация

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