orthogonalProjection_vsub_mem_direction_orthogonal

English

The vector from p to its projection lies in the orthogonal direction to s.

Русский

Вектор от p к её проекции лежит в ортогональном направлении к s.

LaTeX

$$$ p -\!\!>\!\! orthogonalProjection s p \in s.direction^\perp $$$

Lean4

/-- Subtracting `p` from its `orthogonalProjection` produces a result
in the orthogonal direction. -/
theorem orthogonalProjection_vsub_mem_direction_orthogonal (s : AffineSubspace ℝ P) [Nonempty s]
    [s.direction.HasOrthogonalProjection] (p : P) : (orthogonalProjection s p : P) -ᵥ p ∈ s.directionᗮ :=
  orthogonalProjectionFn_vsub_mem_direction_orthogonal p

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