isLeast_opNNNorm — Mathlib

English

The operator NN-norm ‖f‖₊ is the least element of the set of constants C for which ‖f x‖ ≤ C‖x‖ for all x.

Русский

Норма оператора ‖f‖₊ является наименьшим константoм C, для которого ‖f x‖ ≤ C‖x‖ для всех x.

LaTeX

$$IsLeast {C : ℝ≥0 | ∀ x, ‖f x‖₊ ≤ C * ‖x‖₊} (‖f‖₊)$$

Lean4

theorem isLeast_opNNNorm (f : E →SL[σ₁₂] F) : IsLeast {C : ℝ≥0 | ∀ x, ‖f x‖₊ ≤ C * ‖x‖₊} ‖f‖₊ := by
  simpa only [← opNNNorm_le_iff] using isLeast_Ici

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