sSup_unit_ball_eq_norm — Mathlib

English

For a continuous linear map f, the supremum of the real norms ‖f x‖ over x in the unit ball equals the real operator norm ‖f‖.

Русский

Пусть f — непрерывно линейное отображение. Тогда супремум по значениям нормы ‖f x‖ на единичном шаре равен реальной операторной норме ‖f‖.

LaTeX

$$$\\forall f: E \\to SL[\\sigma_{12}] F,\\ sSup\\big(\\{\\|f x\\| : \\|x\\| < 1\\}\\big) = \\|f\\|.$$$

Lean4

theorem sSup_unit_ball_eq_norm (f : E →SL[σ₁₂] F) : sSup ((fun x => ‖f x‖) '' ball 0 1) = ‖f‖ := by
  simpa only [NNReal.coe_sSup, Set.image_image] using NNReal.coe_inj.2 f.sSup_unit_ball_eq_nnnorm

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