sign_signedInfDist_lineMap_incenter_touchpoint

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

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