signedInfDist_incenter — Mathlib

English

The distance between the incenter and the touchpoint on a chosen face equals the inradius.

Русский

Расстояние между инцентром и touchpoint на выбранной грани равно инрадиусу.

LaTeX

$$dist s.incenter (s.touchpoint ∅ i) = s.inradius$$

Lean4

/-- The signed distance between the incenter and its projection in the plane of each face is the
inradius.

In other words, the incenter is _internally_ tangent to the faces. -/
theorem signedInfDist_incenter (i : Fin (n + 1)) : s.signedInfDist i s.incenter = s.inradius :=
  by
  rw [incenter, exsphere_center, s.excenterExists_empty.signedInfDist_excenter]
  simp (discharger := positivity)

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