adjoint_comp — Mathlib

English

The adjoint of a composition matches the reverse composition of adjoints: adjoint (A ∘ B) = B† ∘ A†.

Русский

Сопряжённый композиции равен композиции сопряжённых в обратном порядке: (A ∘ B)† = B† ∘ A†.

LaTeX

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

Lean4

/-- The adjoint of the composition of two operators is the composition of the two adjoints
in reverse order. -/
@[simp]
theorem adjoint_comp (A : F →L[𝕜] G) (B : E →L[𝕜] F) : (A ∘L B)† = B† ∘L A† :=
  by
  ext v
  refine ext_inner_left 𝕜 fun w => ?_
  simp only [adjoint_inner_right, ContinuousLinearMap.coe_comp', Function.comp_apply]

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