inner_starProjection_left_eq_right

English

The star projection onto K is a symmetric projection; i.e., it is self-adjoint.

Русский

Звёздочная проекция на K является симметричной проекцией, то есть самосопряженной.

LaTeX

$$$ K.starProjection.IsSymmetricProjection. $$$

Lean4

/-- The orthogonal projection is self-adjoint. -/
theorem inner_starProjection_left_eq_right [K.HasOrthogonalProjection] (u v : E) :
    ⟪K.starProjection u, v⟫ = ⟪u, K.starProjection v⟫ := by
  simp_rw [starProjection_apply, ← inner_orthogonalProjection_eq_of_mem_left,
    inner_orthogonalProjection_eq_of_mem_right]

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