orthogonalProjectionSpan_faceOpposite_eq_point_rev

English

For a 1-simplex, the projection onto the opposite face equals the opposite vertex.

Русский

Для 1-симплекса проекция на противоположную грань равна противоположной вершине.

LaTeX

$$$$ (s.faceOpposite i).\operatorname{orthogonalProjectionSpan}(p) = s.points(i^{\mathrm{rev}}). $$$$

Lean4

theorem orthogonalProjectionSpan_faceOpposite_eq_point_rev (s : Simplex ℝ P 1) (i : Fin 2) (p : P) :
    (s.faceOpposite i).orthogonalProjectionSpan p = s.points i.rev := by simp [faceOpposite_point_eq_point_rev]

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