sSup_unitClosedBall_eq_norm — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall f: E \\to SL[\\sigma_{12}] F,\\ sup_{\\|x\\|\\le 1} \\|f x\\| = \\|f\\|.$$$

Lean4

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

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