toIsBoundedSMul — Mathlib

English

If α is a seminormed ring and β a normed add group with a module structure, then IsBoundedSmul α β holds, i.e., the scalar action is bounded by the operator norm: ∥r • x∥ ≤ ∥r∥ ∥x∥ for all r,x.

Русский

Пусть α — полунормированное кольцо и β — нормированная абелева группа с действием по модулю: действие по скалярам ограничено, то есть ∥r • x∥ ≤ ∥r∥ ∥x∥ для всех r,x.

LaTeX

$$$$\\|r \\cdot x\\| \\leq \\|r\\| \\cdot \\|x\\|.$$$$

Lean4

instance toIsBoundedSMul : IsBoundedSMul α β :=
  .of_norm_smul_le fun r x ↦ (norm_smul r x).le

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