English
The weights used to express the touchpoint as an affine combination of vertices sum to one.
Русский
Сумма весов касательных точек по всем вершинам относительно i равна единице.
LaTeX
$$$ \sum_j s.touchpointWeights(\text{signs}, i, j) = 1 $$$
Lean4
theorem exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter {p : P}
(hp : p ∈ affineSpan ℝ (Set.range s.points)) :
(∃ r : ℝ, ∀ i, dist p ((s.faceOpposite i).orthogonalProjectionSpan p) = r) ↔
∃ signs, s.ExcenterExists signs ∧ p = s.excenter signs :=
by
simp_rw [← abs_signedInfDist_eq_dist_of_mem_affineSpan_range _ hp]
refine ⟨?_, ?_⟩
· rintro ⟨r, h⟩
have h' : ∀ i, s.signedInfDist i p = r ∨ s.signedInfDist i p = -r := fun i ↦ eq_or_eq_neg_of_abs_eq (h i)
refine ⟨{i ∈ (Finset.univ : Finset (Fin (n + 1))) | s.signedInfDist i p = -r}, ?_⟩
apply (s.exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter hp).1
refine ⟨r, ?_⟩
grind [Finset.mem_filter_univ]
· rintro ⟨signs, h⟩
replace h := (s.exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter hp).2 h
rcases h with ⟨r, h⟩
refine ⟨|r|, ?_⟩
simp [h, abs_ite]
