spectralAlgNorm_of_finiteDimensional_normal_def

English

For IsUltrametricDist K, the algebra norm on L given by spectralAlgNorm_of_finiteDimensional_normal coincides with the spectral norm on L.

Русский

Пусть K имеет ультраметрику, тогда алгебральная норма, заданная spectralAlgNorm_of_finiteDimensional_normal, совпадает со спектральной нормой на L.

LaTeX

$$$(\text{spectralAlgNorm\_of\_finiteDimensional\_normal }\ K \ L)(x) = \operatorname{spectralNorm}_{K,L}(x) \quad \text{для всех } x \in L$$$

Lean4

theorem spectralAlgNorm_of_finiteDimensional_normal_def [IsUltrametricDist K] (x : L) :
    spectralAlgNorm_of_finiteDimensional_normal K L x = spectralNorm K L x :=
  rfl

Похожие утверждения