exsphere_univ — Mathlib

English

The exsphere taken over all vertex signs (universal) equals the insphere.

Русский

Эксерфера для полного набора знаков равна вписанной сфере.

LaTeX

$$exsphere univ = insphere$$

Lean4

@[simp]
theorem exsphere_univ : s.exsphere Finset.univ = s.insphere :=
  by
  rw [exsphere, ← Finset.compl_empty, excenterWeightsUnnorm_compl, excenterWeights_compl]
  simp [Pi.neg_apply, Finset.sum_neg_distrib, insphere, exsphere]

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