exradius_univ

Mathlib.Geometry.Euclidean.Incenter

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

English

For any simplex s, the exradius with respect to all faces equals the inradius of s.

Русский

Для любого симплекса s эксрадиус по всем граням равен инрадиусу.

LaTeX

$$$s\,\mathrm{exradius}(\mathrm{Finset.univ}) = s\,\mathrm{inradius}$$$

Lean4

@[simp]
theorem exradius_univ : s.exradius Finset.univ = s.inradius := by rw [exradius, exsphere_univ, insphere_radius]

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

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

Разделы

Аффилиация

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