continuous_decomposeProdAdjoint — Mathlib

English

The adjoint decomposition into self-adjoint and skew-adjoint parts is continuous.

Русский

Разложение смежного оператора на самосопряжённую и кососопряжённую части непрерывно.

LaTeX

$$$\text{Continuous}(\text{StarModule.decomposeProdAdjoint}(R,A)).$$$

Lean4

theorem continuous_decomposeProdAdjoint [IsTopologicalAddGroup A] [ContinuousStar A] [ContinuousConstSMul R A] :
    Continuous (StarModule.decomposeProdAdjoint R A) :=
  (continuous_selfAdjointPart R A).prodMk (continuous_skewAdjointPart R A)

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