orthogonalProjectionFn_inner_eq_zero

English

For any w ∈ K, ⟪v−p, w⟫ = 0 where p = K.orthogonalProjectionFn(v).

Русский

Для любой w∈K верно ⟪v−p, w⟫ = 0, где p = K.orthogonalProjectionFn(v).

LaTeX

$$⟪v−K.orthogonalProjectionFn(v), w⟫ = 0 for all w ∈ K$$

Lean4

/-- The characterization of the unbundled orthogonal projection.  This
lemma is only intended for use in setting up the bundled version
and should not be used once that is defined. -/
theorem orthogonalProjectionFn_inner_eq_zero (v : E) : ∀ w ∈ K, ⟪v - K.orthogonalProjectionFn v, w⟫ = 0 :=
  (K.mem_orthogonal' _).1 (HasOrthogonalProjection.exists_orthogonal (K := K) v).choose_spec.right

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