signedInfDist_apply_self — Mathlib

English

For a simplex s and index i, the signedInfDist evaluated at the i-th vertex equals the distance from that vertex to the opposite face's projection. Formally: s.signedInfDist i (s.points i) = || s.points i −ᵥ (s.faceOpposite i).orthogonalProjectionSpan (s.points i) ||.

Русский

Для простейшего s и индекса i значение s.signedInfDist, взятое в вершине i, равно расстоянию от этой вершины до проекции на противоположную грань.

LaTeX

$$$s.signedInfDist i (s.points i) = \|s.points i -\! (s.faceOpposite i).orthogonalProjectionSpan (s.points i)\|$$$

Lean4

theorem signedInfDist_apply_self :
    s.signedInfDist i (s.points i) = ‖s.points i -ᵥ (s.faceOpposite i).orthogonalProjectionSpan (s.points i)‖ :=
  (AffineSubspace.signedInfDist_apply_self _ _).trans <| by simp [orthogonalProjectionSpan]

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