inner_orthogonalProjection_eq_of_mem_right

English

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

Русский

Для любого u ∈ K и v ∈ E выполняется ⟪P_K v, u⟫ = ⟪v, u⟫.

LaTeX

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

Lean4

@[simp high]
theorem inner_orthogonalProjection_eq_of_mem_right [K.HasOrthogonalProjection] (u : K) (v : E) :
    ⟪K.orthogonalProjection v, u⟫ = ⟪v, u⟫ :=
  calc
    ⟪K.orthogonalProjection v, u⟫ = ⟪K.starProjection v, u⟫ := K.coe_inner _ _
    _ = ⟪K.starProjection v, u⟫ + ⟪v - K.starProjection v, u⟫ := by
      rw [starProjection_inner_eq_zero _ _ (Submodule.coe_mem _), add_zero]
    _ = ⟪v, u⟫ := by
      rw [← inner_add_left, add_sub_cancel]
        -- The priority should be higher than `Submodule.coe_inner`.

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