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
@[implicit_reducible]
noncomputable instance BoundedContinuousFunction.instNonUnitalCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [NonUnitalCStarAlgebra A] :
NonUnitalCStarAlgebra (BoundedContinuousFunction α A)
Equations
  • One or more equations did not get rendered due to their size.
source
@[implicit_reducible]
noncomputable instance BoundedContinuousFunction.instNonUnitalCommCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [NonUnitalCommCStarAlgebra A] :
NonUnitalCommCStarAlgebra (BoundedContinuousFunction α A)
Equations
  • One or more equations did not get rendered due to their size.
source
@[implicit_reducible]
noncomputable instance BoundedContinuousFunction.instCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CStarAlgebra A] :
CStarAlgebra (BoundedContinuousFunction α A)
Equations
  • One or more equations did not get rendered due to their size.
source
@[implicit_reducible]
noncomputable instance BoundedContinuousFunction.instCommCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CommCStarAlgebra A] :
CommCStarAlgebra (BoundedContinuousFunction α A)
Equations
  • One or more equations did not get rendered due to their size.
source
@[implicit_reducible]
noncomputable instance ContinuousMap.instNonUnitalCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CompactSpace α] [NonUnitalCStarAlgebra A] :
NonUnitalCStarAlgebra C(α, A)
Equations
  • One or more equations did not get rendered due to their size.
source
@[implicit_reducible]
noncomputable instance ContinuousMap.instNonUnitalCommCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CompactSpace α] [NonUnitalCommCStarAlgebra A] :
NonUnitalCommCStarAlgebra C(α, A)
Equations
  • One or more equations did not get rendered due to their size.
source
@[implicit_reducible]
noncomputable instance ContinuousMap.instCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CompactSpace α] [CStarAlgebra A] :
CStarAlgebra C(α, A)
Equations
  • One or more equations did not get rendered due to their size.
source
@[implicit_reducible]
noncomputable instance ContinuousMap.instCommCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [CompactSpace α] [CommCStarAlgebra A] :
CommCStarAlgebra C(α, A)
Equations
  • One or more equations did not get rendered due to their size.
source
@[implicit_reducible]
noncomputable instance ZeroAtInftyContinuousMap.instNonUnitalCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [NonUnitalCStarAlgebra A] :
NonUnitalCStarAlgebra (ZeroAtInftyContinuousMap α A)
Equations
  • One or more equations did not get rendered due to their size.
source
@[implicit_reducible]
noncomputable instance ZeroAtInftyContinuousMap.instNonUnitalCommCStarAlgebra {α : Type u_1} {A : Type u_2} [TopologicalSpace α] [NonUnitalCommCStarAlgebra A] :
NonUnitalCommCStarAlgebra (ZeroAtInftyContinuousMap α A)
Equations
  • One or more equations did not get rendered due to their size.