inradius_pos

Mathlib.Geometry.Euclidean.Incenter

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

English

The inradius of s is strictly positive.

Русский

Инрадиус симплекса s положителен.

LaTeX

$$0 < s.inradius$$

Lean4

theorem inradius_pos : 0 < s.inradius :=
  s.excenterExists_empty.exradius_pos

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

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

Разделы

Аффилиация

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