adjointAux_apply — Mathlib

English

Applying the adjoint twice yields the original operator, i.e., the adjoint is involutive on bounded operators.

Русский

При приложении сопряжённого оператора дважды получаем исходный оператор; сопряжение является инволютивным на ограниченных операторах.

LaTeX

$$$$ (A^{\\dagger})^{\\dagger} = A. $$$$

Lean4

@[simp]
theorem adjointAux_apply (A : E →L[𝕜] F) (x : F) :
    adjointAux A x = ((toDual 𝕜 E).symm : StrongDual 𝕜 E → E) ((toSesqForm A) x) :=
  rfl

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