affineCombination_eq_touchpoint_iff

English

The signs of touchpoint and excenter weights agree as predicted by the excenter configuration.

Русский

Знак весов точек касания совпадает со знаком весов эксцентра при сравнении точек касания и экцентров.

LaTeX

$$$ \text{sign}( s.touchpointWeights(\text{signs}, i, j) ) = \text{sign}( s.excenterWeights(\text{signs}, j) ) $$$

Lean4

@[simp]
theorem affineCombination_eq_touchpoint_iff {signs : Finset (Fin (n + 1))} {i : Fin (n + 1)} {w : Fin (n + 1) → ℝ}
    (hw : ∑ j, w j = 1) :
    Finset.univ.affineCombination ℝ s.points w = s.touchpoint signs i ↔ w = s.touchpointWeights signs i :=
  by
  constructor
  · rw [← s.affineCombination_touchpointWeights]
    exact fun h ↦
      (affineIndependent_iff_eq_of_fintype_affineCombination_eq ℝ s.points).1 s.independent _ _ hw
        (s.sum_touchpointWeights _ _) h
  · rintro rfl
    simp

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