vsub_orthogonalProjection_mem_direction

English

The intersection identity holds: the intersection equals the singleton of the projection point.

Русский

Пересечение равно множеству-одному точке проекции.

LaTeX

$$$ (s : Set P) \cap mk' p s.direction^\perp = { \uparrow(\operatorname{orthogonalProjection} s p) } $$$

Lean4

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

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