abs_signedInfDist_eq_dist_of_mem_affineSpan_range

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

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