touchpoint_mem_insphere — Mathlib

English

Let s be a real affine simplex. Then for every vertex index i (in {0,...,n}), the touchpoint with the empty sign set lies on the insphere of s.

Русский

Пусть s — аффинный симплекс над Real. Тогда для каждого индекса вершины i (от 0 до n) точка касания с пустым набором знаков принадлежит вписанной сфере s.

LaTeX

$$$ \forall i \in \{0,1,\dots,n\},\; s.touchpoint(\emptyset,i) \in s.insphere $$$

Lean4

theorem touchpoint_mem_insphere (i : Fin (n + 1)) : s.touchpoint ∅ i ∈ s.insphere :=
  s.excenterExists_empty.touchpoint_mem_exsphere _

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