continuous_decomposeProdAdjoint_symm

English

There exists a continuous inverse for the decomposition of elements in a star module into their self-adjoint and skew-adjoint parts; equivalently, the inverse map of the decomposition is continuous.

Русский

Существуют непрерывное отображение-обратное к разложению элементов звёздового модуля на их самосопряжённые и кососопряжённые части; эквивалентно, обратное к этому разложению непрерывно.

LaTeX

$$$\\operatorname{Continuous}\\big( (\\operatorname{decomposeProdAdjoint}(R,A))^{-1} \\big)$$$

Lean4

theorem continuous_decomposeProdAdjoint_symm [ContinuousAdd A] :
    Continuous (StarModule.decomposeProdAdjoint R A).symm :=
  (continuous_subtype_val.comp continuous_fst).add (continuous_subtype_val.comp continuous_snd)

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