le_of_opNorm_le

Mathlib.Analysis.Normed.Operator.Basic

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

English

If ‖f‖ ≤ a and ‖x‖ ≤ b, then ‖f x‖ ≤ a b.

Русский

Если ‖f‖ ≤ a и ‖x‖ ≤ b, то ‖f x‖ ≤ a b.

LaTeX

$$$\\|f x\\| \\le a \\; \\|x\\| \\le a b$$$

Lean4

theorem le_of_opNorm_le {c : ℝ} (h : ‖f‖ ≤ c) (x : E) : ‖f x‖ ≤ c * ‖x‖ :=
  f.le_of_opNorm_le_of_le h le_rfl

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

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

Разделы

Аффилиация

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