selfAdjointPartL — Mathlib

English

The self-adjoint part map is a continuous linear map from A to the self-adjoint part of A.

Русский

Отображение на самосопряжённую часть является непрерывным линейным отображением из A в самосопряжённую часть A.

LaTeX

$$$L: A \\to_L[R] \\operatorname{selfAdjoint}(A),\\quad L(x)=\\operatorname{selfAdjointPart}(x).$$$

Lean4

/-- The self-adjoint part of an element of a star module, as a continuous linear map. -/
@[simps! -isSimp]
def selfAdjointPartL [ContinuousAdd A] [ContinuousStar A] [ContinuousConstSMul R A] : A →L[R] selfAdjoint A
    where
  toLinearMap := selfAdjointPart R
  cont := continuous_selfAdjointPart _ _

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