orthogonalProjectionSpan_eq_point

English

For a 0-simplex, the orthogonal projection span of p equals its vertex point.

Русский

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

LaTeX

$$$$s.orthogonalProjectionSpan(p) = s.points(0).$$$$

Lean4

@[simp]
theorem orthogonalProjectionSpan_eq_point (s : Simplex ℝ P 0) (p : P) : s.orthogonalProjectionSpan p = s.points 0 :=
  by
  rw [orthogonalProjectionSpan]
  convert orthogonalProjection_affineSpan_singleton _ _
  simp [Fin.fin_one_eq_zero]

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