English
If F is a class of algebra homomorphisms from a normed algebra A into the base field, then each element of F acts as a bounded linear functional; thus F carries a natural continuous linear map structure with the operator bound governed by the unit element.
Русский
Если F — множество алгебраических гомоморфизмов из нормированной алгебры A в базовое поле, то каждый элемент F является ограниченным линейным функционалом; поэтому F обладает естественной структурой непрерывного линейного отображения, контролируемой нормой единицы.
LaTeX
$$$\\text{F has }\\text{ContinuousLinearMapClass } 𝕜\, A \\, 𝕜$ with bound determined by ‖1‖.$$
Lean4
instance (priority := 100) [FunLike F A 𝕜] [AlgHomClass F 𝕜 A 𝕜] : ContinuousLinearMapClass F 𝕜 A 𝕜 :=
{ AlgHomClass.linearMapClass with
map_continuous := fun φ =>
AddMonoidHomClass.continuous_of_bound φ ‖(1 : A)‖ fun a =>
mul_comm ‖a‖ ‖(1 : A)‖ ▸ spectrum.norm_le_norm_mul_of_mem (apply_mem_spectrum φ _) }
