instStarRing — Mathlib

English

The bounded continuous functions α → β form a C*-algebra under pointwise operations, with the C*-norm identity: ∥f* f∥ ≤ ∥f∥^2.

Русский

Ограниченно непрерывные функции образуют C*-алгебру с точечными операциями и нормой C*-типа, выполняется неравенство: ∥f* f∥ ≤ ∥f∥^2.

LaTeX

$$$$ \|f^* f\| \le \|f\|^2.$$$$

Lean4

instance instStarRing [NormedStarGroup β] : StarRing (α →ᵇ β)
    where
  __ := instStarAddMonoid
  star_mul f g := ext fun x ↦ star_mul (f x) (g x)

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