instCommCStarAlgebra — Mathlib

English

If A is a commutative C*-algebra, then the bounded continuous A-valued functions α →ᵇ A form a commutative C*-algebra.

Русский

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

LaTeX

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

Lean4

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

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