English
If two vertex indices are different, the corresponding touchpoint cannot lie in the span of the opposite face.
Русский
Если i ≠ j, то точка касания по i не принадлежит аффинному пространству противоположной грани j.
LaTeX
$$$ (i \neq j) \Rightarrow s.touchpoint(\text{signs}, i) \notin \operatorname{affineSpan}_{\mathbb{R}}(\mathrm{Set.range}(s.faceOpposite(j).points)) $$$
Lean4
theorem touchpoint_notMem_affineSpan_of_ne {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs)
{i j : Fin (n + 1)} (hne : i ≠ j) : s.touchpoint signs i ∉ affineSpan ℝ (Set.range (s.faceOpposite j).points) :=
fun hm ↦
h.touchpoint_injective.ne hne ((h.isTangentAt_touchpoint j).eq_of_mem_of_mem (h.touchpoint_mem_exsphere i) hm)