sign_signedInfDist_touchpoint — Mathlib

English

Signed distance relations governed by line maps identify either the excenter or the incenter depending on the sign pattern.

Русский

Расстояния, полученные через отображения вдоль линии, эквивалентны эксцентрическому/инцентровому случаю при разных множествах знаков.

LaTeX

$$$ \text{Equiv}( s.signedInfDist, s.excenter) \text{ or } \text{Incenter} $$$

Lean4

theorem sign_signedInfDist_touchpoint {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) {i j : Fin (n + 1)}
    (hne : i ≠ j) :
    SignType.sign (s.signedInfDist j (s.touchpoint signs i)) = SignType.sign (s.signedInfDist j (s.excenter signs)) :=
  by
  rw [← h.sign_signedInfDist_lineMap_excenter_touchpoint hne (r := 1) ⟨zero_le_one, le_rfl⟩]
  simp

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