instCommCStarAlgebra

Mathlib.Analysis.CStarAlgebra.ContinuousMap

URI: https://scilib.ai/kg/mathlib#ContinuousMap.instCommCStarAlgebra

English

If A is a commutative C*-algebra, then the continuous map algebra C(α, A) is a commutative C*-algebra.

Русский

Если A — коммутативная C*-алгебра, то алгебра непрерывных отображений C(α, A) является коммутативной C*-алгеброй.

LaTeX

$$$$C(\alpha, A) \text{ is a CommCStarAlgebra}$$$$

Lean4

instance [CommCStarAlgebra A] : CommCStarAlgebra C(α, A) where

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

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

Разделы

Аффилиация

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