excenter_univ — Mathlib

English

Let s be an affine simplex in a Euclidean space. Then the excenter corresponding to all faces (the full index set) coincides with the incenter of s.

Русский

Пусть s — аффинальный симплекс в евклидовом пространстве. Тогда эксцентр, соответствующий всем граням (полный набор индексов), совпадает с инцентром s.

LaTeX

$$$s\,\mathrm{excenter}(\mathrm{Finset.univ}) = s\,\mathrm{incenter}$$$

Lean4

@[simp]
theorem excenter_univ : s.excenter Finset.univ = s.incenter := by rw [excenter, exsphere_univ, insphere_center]

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