inner_orthogonalProjection_eq_of_mem_left

English

For u ∈ K and v ∈ E, ⟪u, K.orthogonalProjection v⟫ = ⟪u, v⟫.

Русский

Для u ∈ K и v ∈ E имеет место ⟪u, P_K v⟫ = ⟪u, v⟫.

LaTeX

$$$ \langle u, K.orthogonalProjection(v) \rangle = \langle u, v \rangle, \quad u \in K. $$$

Lean4

@[simp high]
theorem inner_orthogonalProjection_eq_of_mem_left [K.HasOrthogonalProjection] (u : K) (v : E) :
    ⟪u, K.orthogonalProjection v⟫ = ⟪(u : E), v⟫ := by
  rw [← inner_conj_symm, ← inner_conj_symm (u : E), inner_orthogonalProjection_eq_of_mem_right]

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