exradius_pos

Mathlib.Geometry.Euclidean.Incenter

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

English

If an excenter exists for the given signs, the exradius is strictly positive.

Русский

Если существует экцентер при заданном наборе знаков, эксрадиус положителен.

LaTeX

$$0 < s.exradius signs$$

Lean4

theorem exradius_pos {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) : 0 < s.exradius signs :=
  abs_pos.2 (inv_ne_zero h)

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

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

Разделы

Аффилиация

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