le_of_opNorm_le — Mathlib

English

If ‖f‖ ≤ c, then for all x, ‖f x‖ ≤ c ‖x‖. (Equivalent formulation of le_opNorm.)

Русский

Если ‖f‖ ≤ c, то для всех x выполняется ‖f x‖ ≤ c‖x‖. (Эквивалентно предшествующему.)

LaTeX

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

Lean4

theorem le_of_opNorm_le {c : ℝ} (h : ‖f‖ ≤ c) (x : V₁) : ‖f x‖ ≤ c * ‖x‖ :=
  (f.le_opNorm x).trans (by gcongr)

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