orthogonalProjectionFn_mem — Mathlib

English

For any v, the unbundled projection K.orthogonalProjectionFn(v) lies in K.

Русский

Для любого вектора v неразложенная проекция K.orthogonalProjectionFn(v) принадлежит K.

LaTeX

$$K.orthogonalProjectionFn(v) ∈ K$$

Lean4

/-- The unbundled orthogonal projection is 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 (v : E) : K.orthogonalProjectionFn v ∈ K :=
  (HasOrthogonalProjection.exists_orthogonal (K := K) v).choose_spec.left

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