Mathlib Map

Structures · Analysis

NonUnitalClosedEmbeddingContinuousFunctionalCalculus

A class for the non-unital continuous functional calculus which requires the homomorphisms C(quasispectrum 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 non-unital 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.NonUnital
Shape
3 explicit arguments · adds isClosedEmbedding

Extends1

Extended by0

Nothing extends this class yet.

Concrete types that are instances0

No instance on a concrete type; it is reached through other classes.

How is a type an instance?

Loading the hierarchy index…

Assumed by7

Ancestors1