le_opNNNorm

Mathlib.Analysis.Normed.Operator.NNNorm

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.le_opNNNorm

English

For any f and x, the NN-norm of f x is bounded by the product of the NN-norm of f and the NN-norm of x.

Русский

Для любых f и x ‖f x‖₊ ≤ ‖f‖₊ · ‖x‖₊.

LaTeX

$$$\\|f x\\|_{+} ≤ \\|f\\|_{+} \\cdot \\|x\\|_{+}$$$

Lean4

theorem le_opNNNorm (f : E →SL[σ₁₂] F) (x : E) : ‖f x‖₊ ≤ ‖f‖₊ * ‖x‖₊ :=
  f.le_opNorm x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru