Structures · Analysis

ContinuousMapZero.UniqueHom

A class guaranteeing that the non-unital continuous functional calculus is uniquely determined by the properties that it is a continuous non-unital star algebra homomorphism mapping the (restriction of) the identity to a. This is the necessary tool used to establish cfcₙHom_comp and the more common variant cfcₙ_comp. This class will have instances in each of the common cases ℂ, ℝ and ℝ≥0 as a consequence of the Stone-Weierstrass theorem.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Shape

2 explicit arguments · adds eq_of_continuous_of_map_id