English
For p in the affine span of the vertex range, the absolute signedInfDist equals the distance from p to the projection of p onto the opposite face.
Русский
Для p в афинальном охвате диапазона вершин, |s.signedInfDist i p| = dist(p, proj_{opp face}(p)).
LaTeX
$$$|s.signedInfDist i p| = \operatorname{dist}\bigl(p, (s.faceOpposite i).orthogonalProjectionSpan(p)\bigr)$$$
Lean4
theorem abs_signedInfDist_eq_dist_of_mem_affineSpan_range {p : P} (h : p ∈ affineSpan ℝ (Set.range s.points)) :
|s.signedInfDist i p| = dist p ((s.faceOpposite i).orthogonalProjectionSpan p) :=
by
rw [signedInfDist, AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insert, orthogonalProjectionSpan]
· simp_rw [range_faceOpposite_points]
rw [affineSpan_insert_affineSpan]
convert h
exact Set.insert_image_compl_eq_range s.points i