isTangentAt_insphere_touchpoint — Mathlib

English

For every i, the touchpoint corresponding to i lies on the insphere, i.e., the insphere is tangent at that point to the corresponding face-span.

Русский

Для каждого i касательная точка по i лежит на вписанной сфере, то есть сфера касается этой точки.

LaTeX

$$$ (s.insphere).IsTangentAt (s.touchpoint(\emptyset,i)) (\operatorname{affineSpan}_{\mathbb{R}}(\mathrm{Set.range}(s.faceOpposite(i).points))) $$$

Lean4

theorem isTangentAt_insphere_touchpoint (i : Fin (n + 1)) :
    s.insphere.IsTangentAt (s.touchpoint ∅ i) (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :=
  s.excenterExists_empty.isTangentAt_touchpoint i

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