instCStarAlgebra

Mathlib.Analysis.CStarAlgebra.ContinuousMap

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.instCStarAlgebra

English

If A is a C*-algebra, then the space of bounded continuous A-valued functions on α, α →ᵇ A, forms a C*-algebra.

Русский

Если A — C*-алгебра, то пространство ограниченных непрерывных функций α в A образуют C*-алгебру.

LaTeX

$$$$\text{BoundedContinuousFunction}(\alpha, A) \text{ is a } C^*\text{-algebra}$$$$

Lean4

instance [CStarAlgebra A] : CStarAlgebra (α →ᵇ A) where

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

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

Разделы

Аффилиация

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