orthogonalProjection_vadd_smul_vsub_orthogonalProjection

English

A scalar multiple added to a point in the orthogonal direction remains consistent under projection.

Русский

Умножение скаляра и добавление к точке вдоль ортогонального направления сохраняет проекцию.

LaTeX

$$$ orthogonalProjection s (r \cdot v + p) = p $ при hv$$

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 {s : AffineSubspace ℝ P} [Nonempty s]
    [s.direction.HasOrthogonalProjection] {p₁ : P} (p₂ : P) (r : ℝ) (hp : p₁ ∈ s) :
    orthogonalProjection s (r • (p₂ -ᵥ orthogonalProjection s p₂ : V) +ᵥ p₁) = ⟨p₁, hp⟩ :=
  orthogonalProjection_vadd_eq_self hp (Submodule.smul_mem _ _ (vsub_orthogonalProjection_mem_direction_orthogonal s _))

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