ratio_le_opNorm — Mathlib

English

Let f be a bounded additive group homomorphism between seminormed spaces. Then for every x, the ratio of the norms satisfies ||f x|| ≤ ||f|| · ||x||, hence ||f x|| / ||x|| ≤ ||f|| (in particular, for x ≠ 0).

Русский

Пусть f — ограниченный гомоморфизм групп между семинормированными пространствами. Тогда для любого x выполняется неравенство ||f x|| ≤ ||f|| · ||x||, следовательно ||f x|| / ||x|| ≤ ||f|| (и особенно для x ≠ 0).

LaTeX

$$$$ \forall x,\ \|f x\| \le \|f\|\ \|x\| $$$$

Lean4

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

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