Documentation

Mathlib.Analysis.CStarAlgebra.ContinuousMap

C⋆-algebras of continuous functions #

We place these here because, for reasons related to the import hierarchy, they cannot be placed in earlier files.

source
instance BoundedContinuousFunction.instNonUnitalCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [NonUnitalCStarAlgebra A] :
NonUnitalCStarAlgebra (BoundedContinuousFunction α A)
Equations
  • BoundedContinuousFunction.instNonUnitalCStarAlgebra = NonUnitalCStarAlgebra.mk
source
instance BoundedContinuousFunction.instNonUnitalCommCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [NonUnitalCommCStarAlgebra A] :
NonUnitalCommCStarAlgebra (BoundedContinuousFunction α A)
Equations
  • BoundedContinuousFunction.instNonUnitalCommCStarAlgebra = NonUnitalCommCStarAlgebra.mk
source
instance BoundedContinuousFunction.instCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CStarAlgebra A] :
CStarAlgebra (BoundedContinuousFunction α A)
Equations
  • BoundedContinuousFunction.instCStarAlgebra = CStarAlgebra.mk
source
instance BoundedContinuousFunction.instCommCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CommCStarAlgebra A] :
CommCStarAlgebra (BoundedContinuousFunction α A)
Equations
  • BoundedContinuousFunction.instCommCStarAlgebra = CommCStarAlgebra.mk
source
instance ContinuousMap.instNonUnitalCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CompactSpace α] [NonUnitalCStarAlgebra A] :
NonUnitalCStarAlgebra C(α, A)
Equations
  • ContinuousMap.instNonUnitalCStarAlgebra = NonUnitalCStarAlgebra.mk
source
instance ContinuousMap.instNonUnitalCommCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CompactSpace α] [NonUnitalCommCStarAlgebra A] :
NonUnitalCommCStarAlgebra C(α, A)
Equations
  • ContinuousMap.instNonUnitalCommCStarAlgebra = NonUnitalCommCStarAlgebra.mk
source
instance ContinuousMap.instCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CompactSpace α] [CStarAlgebra A] :
CStarAlgebra C(α, A)
Equations
  • ContinuousMap.instCStarAlgebra = CStarAlgebra.mk
source
instance ContinuousMap.instCommCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CompactSpace α] [CommCStarAlgebra A] :
CommCStarAlgebra C(α, A)
Equations
  • ContinuousMap.instCommCStarAlgebra = CommCStarAlgebra.mk
source
instance ZeroAtInftyContinuousMap.instNonUnitalCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [NonUnitalCStarAlgebra A] :
NonUnitalCStarAlgebra (ZeroAtInftyContinuousMap α A)
Equations
  • ZeroAtInftyContinuousMap.instNonUnitalCStarAlgebra = NonUnitalCStarAlgebra.mk
source
instance ZeroAtInftyContinuousMap.instNonUnitalCommCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [NonUnitalCommCStarAlgebra A] :
NonUnitalCommCStarAlgebra (ZeroAtInftyContinuousMap α A)
Equations
  • ZeroAtInftyContinuousMap.instNonUnitalCommCStarAlgebra = NonUnitalCommCStarAlgebra.mk