English
There exists a scalar r such that all signed distances from p have the same magnitude r with signs determined by membership in signs; this is equivalent to ExcenterExists and p equals the excenter.
Русский
Существует число r так, что для каждого i подпоследовательность знаков описывает знак расстояния до p как ±r; это эквивалентно существованию эксцентрированного множества и тому, что p совпадает с s.excenter signs.
LaTeX
$$$ \exists r \in \mathbb{R}, \; \forall i, \; s.signedInfDist(i,p) = (\mathbb{1}_{i \in signs} \cdot (-1) \,+\ \mathbb{1}_{i \notin signs} \cdot 1) \cdot r \quad\Leftrightarrow\quad s.ExcenterExists signs \land p = s.excenter signs $$$
Lean4
theorem isTangentAt_insphere_iff_eq_touchpoint {i : Fin (n + 1)} {p : P} :
s.insphere.IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points)) ↔ p = s.touchpoint ∅ i :=
s.excenterExists_empty.isTangentAt_exsphere_iff_eq_touchpoint
