English
The element orthogonalProjectionFn s p lies in mk' p s.direction.orthogonal.
Русский
Элемент orthogonalProjectionFn s p лежит в mk' p s.direction.orthogonal.
LaTeX
$$orthogonalProjectionFn s p ∈ mk' p s.direction.orthogonal$$
Lean4
/-- The `orthogonalProjectionFn` lies in the orthogonal
subspace. This lemma is only intended for use in setting up the
bundled version and should not be used once that is defined. -/
theorem orthogonalProjectionFn_mem_orthogonal {s : AffineSubspace ℝ P} [Nonempty s]
[s.direction.HasOrthogonalProjection] (p : P) : orthogonalProjectionFn s p ∈ mk' p s.directionᗮ :=
by
rw [← mem_coe, ← Set.singleton_subset_iff, ← inter_eq_singleton_orthogonalProjectionFn]
exact Set.inter_subset_right