orthogonalProjection_vadd_smul_vsub_orthogonalProjection

English

The orthogonal projection onto the span of a 0-simplex reduces to the single vertex point.

Русский

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

LaTeX

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

Lean4

/-- Adding a vector to a point in the given subspace, then taking the
orthogonal projection, produces the original point if the vector is a
multiple of the result of subtracting a point's orthogonal projection
from that point. -/
theorem orthogonalProjection_vadd_smul_vsub_orthogonalProjection {n : ℕ} (s : Simplex ℝ P n) {p₁ : P} (p₂ : P) (r : ℝ)
    (hp : p₁ ∈ affineSpan ℝ (Set.range s.points)) :
    s.orthogonalProjectionSpan (r • (p₂ -ᵥ s.orthogonalProjectionSpan p₂ : V) +ᵥ p₁) = ⟨p₁, hp⟩ :=
  EuclideanGeometry.orthogonalProjection_vadd_smul_vsub_orthogonalProjection _ _ _

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