opNorm_le_bound — Mathlib

English

If a linear map f satisfies ||f x|| ≤ M ||x|| for all x and M ≥ 0, then the operator norm of f is at most M.

Русский

Если линейное отображение f удовлетворяет ||f x|| ≤ M ||x|| для всех x и M ≥ 0, то операторная норма ||f|| ≤ M.

LaTeX

$$$$ (0 \le M) \ ∧\ ( \forall x, \|f x\| \le M \|x\| ) \Rightarrow \|f\| \le M $$$$

Lean4

/-- If one controls the norm of every `f x`, then one controls the norm of `f`. -/
theorem opNorm_le_bound {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ x, ‖f x‖ ≤ M * ‖x‖) : ‖f‖ ≤ M :=
  csInf_le bounds_bddBelow ⟨hMp, hM⟩

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