English
The intersection of the subspace through a point and the orthogonal direction is the singleton given by orthogonalProjectionFn.
Русский
Пересечение подпространства через точку и ортогонального направления — это единичный элемент, задаваемый orthogonalProjectionFn.
LaTeX
$$(s : AffineSubspace ℝ P) ∩ mk' p s.directionᗮ = { orthogonalProjectionFn s p }$$
Lean4
/-- The intersection of the subspace and the orthogonal subspace
through the given point is the `orthogonalProjectionFn` of that
point onto the subspace. This lemma is only intended for use in
setting up the bundled version and should not be used once that is
defined. -/
theorem inter_eq_singleton_orthogonalProjectionFn {s : AffineSubspace ℝ P} [Nonempty s]
[s.direction.HasOrthogonalProjection] (p : P) : (s : Set P) ∩ mk' p s.directionᗮ = {orthogonalProjectionFn s p} :=
Classical.choose_spec <|
inter_eq_singleton_of_nonempty_of_isCompl (nonempty_subtype.mp ‹_›) (mk'_nonempty p s.directionᗮ)
(by
rw [direction_mk' p s.directionᗮ]
exact Submodule.isCompl_orthogonal_of_hasOrthogonalProjection)
