le_opNorm_of_le

Mathlib.Analysis.Normed.Group.Hom

URI: https://scilib.ai/kg/mathlib#NormedAddGroupHom.le_opNorm_of_le

English

If ‖f‖ ≤ c, then for all x, ‖f x‖ ≤ c ‖x‖.

Русский

Если ‖f‖ ≤ c, то для каждого x выполняется ‖f x‖ ≤ c ‖x‖.

LaTeX

$$$\\forall c:\\mathbb{R}, \\; \\|f\\| \\le c \\Rightarrow \\forall x,\\ |f x| ≤ c \\cdot \\|x\\|$$$

Lean4

theorem le_opNorm_of_le {c : ℝ} {x} (h : ‖x‖ ≤ c) : ‖f x‖ ≤ ‖f‖ * c :=
  le_trans (f.le_opNorm x) (by gcongr; exact f.opNorm_nonneg)

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

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

Разделы

Аффилиация

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