vsub_orthogonalProjection_mem_direction_orthogonal

English

The vector difference between p and its projection lies in the orthogonal subspace.

Русский

Разность векторов между p и её проекцией лежит в ортогональном подпространстве.

LaTeX

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

Lean4

/-- Subtracting the `orthogonalProjection` from `p` produces a result
in the orthogonal direction. -/
theorem vsub_orthogonalProjection_mem_direction_orthogonal (s : AffineSubspace ℝ P) [Nonempty s]
    [s.direction.HasOrthogonalProjection] (p : P) : p -ᵥ orthogonalProjection s p ∈ s.directionᗮ :=
  direction_mk' p s.directionᗮ ▸ vsub_mem_direction (self_mem_mk' _ _) (orthogonalProjection_mem_orthogonal s p)

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