instCompletelyPositiveMapClass

Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap

URI: https://scilib.ai/kg/mathlib#CompletelyPositiveMap.instCompletelyPositiveMapClass

English

There is a CompletelyPositiveMapClass instance for CompletelyPositiveMap A1 A2.

Русский

Существует инстанс CompletelyPositiveMapClass для CompletelyPositiveMap A1 A2.

LaTeX

$$instCompletelyPositiveMapClass$$

Lean4

instance : CompletelyPositiveMapClass (A₁ →CP A₂) A₁ A₂ where map_cstarMatrix_nonneg' f := f.map_cstarMatrix_nonneg'

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru