English
The sign of the signed distance from the incenter along a line through a touchpoint remains the same.
Русский
Поведение подписанных расстояний вдоль линейного отображения через инцентр дает постоянный знак на точке касания.
LaTeX
$$$ SignType.sign( s.signedInfDist_j( \mathrm{AffineMap.lineMap}( s.incenter, s.touchpoint(\emptyset,i), r) )) = SignType.sign( s.signedInfDist_j( s.incenter )) $$$
Lean4
theorem sign_signedInfDist_lineMap_incenter_touchpoint {i j : Fin (n + 1)} (hne : i ≠ j) {r : ℝ}
(hr : r ∈ Set.Icc 0 1) :
SignType.sign (s.signedInfDist j (AffineMap.lineMap s.incenter (s.touchpoint ∅ i) r)) =
SignType.sign (s.signedInfDist j s.incenter) :=
s.excenterExists_empty.sign_signedInfDist_lineMap_excenter_touchpoint hne hr