adjoint_isFormalAdjoint — Mathlib

English

The adjoint is the formal adjoint; T†.IsFormalAdjoint T holds, i.e., the adjoint satisfies the defining property of a formal adjoint.

Русский

Сопряженный оператор является формальным сопряженным; T†.IsFormalAdjoint T выполняется.

LaTeX

$$T†.IsFormalAdjoint T$$

Lean4

/-- The fundamental property of the adjoint. -/
theorem adjoint_isFormalAdjoint : T†.IsFormalAdjoint T := fun x =>
  (adjoint_apply_of_dense hT x).symm ▸ adjointAux_inner hT x

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