exsphere_empty

Mathlib.Geometry.Euclidean.Incenter

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

English

The exsphere with signs ∅ coincides with the insphere.

Русский

Эксерфера с пустым набором знаков совпадает с вписанной сферой.

LaTeX

$$exsphere ∅ = insphere$$

Lean4

@[simp]
theorem exsphere_empty : s.exsphere ∅ = s.insphere :=
  rfl

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

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

Разделы

Аффилиация

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