le_opNorm — Mathlib

English

For all x, ‖f x‖ ≤ ‖f‖ · ‖x‖; in particular, f is bounded by its operator norm.

Русский

Для всех x выполняется ‖f x‖ ≤ ‖f‖ · ‖x‖; следовательно, f ограничено своей операторной нормой.

LaTeX

$$$\\forall x,\\ ‖f x‖ ≤ ‖f‖ \\cdot ‖x‖$$$

Lean4

/-- The fundamental property of the operator norm: `‖f x‖ ≤ ‖f‖ * ‖x‖`. -/
theorem le_opNorm (x : V₁) : ‖f x‖ ≤ ‖f‖ * ‖x‖ :=
  by
  obtain ⟨C, _Cpos, hC⟩ := f.bound
  replace hC := hC x
  by_cases h : ‖x‖ = 0
  · rwa [h, mul_zero] at hC ⊢
  have hlt : 0 < ‖x‖ := lt_of_le_of_ne (norm_nonneg x) (Ne.symm h)
  exact (div_le_iff₀ hlt).mp (le_csInf bounds_nonempty fun c ⟨_, hc⟩ => (div_le_iff₀ hlt).mpr <| by apply hc)

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