English
For any p, the intersection of s with the affine subspace starting at p in the orthogonal direction to s is exactly the singleton containing the orthogonal projection of p onto s.
Русский
Для любой точки p пересечение s и аффинного подпространства через p с направлением, ортогональным к s, образуют точку-одинец, равную проекции p на s.
LaTeX
$$$ (s : Set P) \cap mk' p s.direction^\perp = \{ \uparrow(\operatorname{orthogonalProjection} s p) \} $$$
Lean4
/-- The intersection of the subspace and the orthogonal subspace
through the given point is the `orthogonalProjection` of that point
onto the subspace. -/
theorem inter_eq_singleton_orthogonalProjection {s : AffineSubspace ℝ P} [Nonempty s]
[s.direction.HasOrthogonalProjection] (p : P) : (s : Set P) ∩ mk' p s.directionᗮ = {↑(orthogonalProjection s p)} :=
by
rw [← orthogonalProjectionFn_eq]
exact inter_eq_singleton_orthogonalProjectionFn p
