ratio_le_opNorm

Mathlib.Analysis.Normed.Operator.Basic

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

English

For any x ≠ 0, the ratio ∥f x∥/∥x∥ is ≤ ∥f∥.

Русский

Для любого x ≠ 0, отношение ∥f x∥/∥x∥ ≤ ∥f∥.

LaTeX

$$$\\frac{\\|f x\\|}{\\|x\\|} \\le \\|f\\|$ for x ≠ 0$$

Lean4

theorem ratio_le_opNorm : ‖f x‖ / ‖x‖ ≤ ‖f‖ :=
  div_le_of_le_mul₀ (norm_nonneg _) f.opNorm_nonneg (le_opNorm _ _)

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

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

Разделы

Аффилиация

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