Structures · Analysis

ClosedEmbeddingContinuousFunctionalCalculus

A class for the continuous functional calculus which requires the homomorphisms C(spectrum R a, R) → A to be closed embeddings, as opposed to only continuous and injective. The primary advantage of this is that one can conclude the range of this map is the closed star subalgebra generated by a. However, unless the topology on A is induced by a C⋆-norm, this is unlikely to occur.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Shape

3 explicit arguments · adds isClosedEmbedding