orthogonalProjection_vsub_mem_direction

English

If p1 ∈ s, then the vector from p1 to the projection of p2 lies in the direction of s.

Русский

Если p1 ∈ s, то вектор от p1 к проекции p2 принадлежит направлению s.

LaTeX

$$$ \uparrow(\operatorname{orthogonalProjection} s p_2 -\!\!>⟨p_1, p_1\in s\rangle) \in s.direction $$$

Lean4

/-- Subtracting a point in the given subspace from the
`orthogonalProjection` produces a result in the direction of the
given subspace. -/
theorem orthogonalProjection_vsub_mem_direction {s : AffineSubspace ℝ P} [Nonempty s]
    [s.direction.HasOrthogonalProjection] {p₁ : P} (p₂ : P) (hp₁ : p₁ ∈ s) :
    ↑(orthogonalProjection s p₂ -ᵥ ⟨p₁, hp₁⟩ : s.direction) ∈ s.direction :=
  (orthogonalProjection s p₂ -ᵥ ⟨p₁, hp₁⟩ : s.direction).2

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