orthogonalProjectionFn_mem — Mathlib

English

The point orthogonalProjectionFn s p lies in s.

Русский

Точка orthogonalProjectionFn s p принадлежит подпространству s.

LaTeX

$$orthogonalProjectionFn s p ∈ s$$

Lean4

/-- The `orthogonalProjectionFn` lies in the given 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 {s : AffineSubspace ℝ P} [Nonempty s] [s.direction.HasOrthogonalProjection] (p : P) :
    orthogonalProjectionFn s p ∈ s :=
  by
  rw [← mem_coe, ← Set.singleton_subset_iff, ← inter_eq_singleton_orthogonalProjectionFn]
  exact Set.inter_subset_left

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