orthogonalProjectionFn — Mathlib

English

The unbundled orthogonal projection is the unique vector in K that satisfies the orthogonality condition with all vectors in K.

Русский

Необъединенная ортогональная проекция — это единственный элемент K, удовлетворяющий условию ортогональности по отношению ко всем элементам K.

LaTeX

$$K.orthogonalProjectionFn u = v iff ∀ w ∈ K, ⟪u−v,w⟫=0$$

Lean4

/-- The orthogonal projection onto a complete subspace, as an
unbundled function. This definition is only intended for use in
setting up the bundled version `orthogonalProjection` and should not
be used once that is defined. -/
def orthogonalProjectionFn (v : E) :=
  (HasOrthogonalProjection.exists_orthogonal (K := K) v).choose

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