English
For a continuous linear map f, the supremum of the nonnegative norms ‖f x‖₊ over all x in the unit ball equals the nnreal operator norm ‖f‖₊.
Русский
Пусть f — непрерывно линейное отображение. Тогда супремум по неотрицательным значениям нормы ‖f x‖₊ над всеми точками единичной сферы равен nn-операторной norme ‖f‖₊.
LaTeX
$$$\\forall f: E \\to SL[\\sigma_{12}] F,\\ sSup\\big(\\{\\|f x\\|_+ : \\|x\\| < 1\\}\\big) = \\|f\\|_+.$$$
Lean4
theorem sSup_unit_ball_eq_nnnorm (f : E →SL[σ₁₂] F) : sSup ((fun x => ‖f x‖₊) '' ball 0 1) = ‖f‖₊ :=
by
refine csSup_eq_of_forall_le_of_forall_lt_exists_gt ((nonempty_ball.mpr zero_lt_one).image _) ?_ fun ub hub => ?_
· rintro - ⟨x, hx, rfl⟩
simpa only [mul_one] using f.le_opNorm_of_le (mem_ball_zero_iff.1 hx).le
· obtain ⟨x, hx, hxf⟩ := f.exists_lt_apply_of_lt_opNNNorm hub
exact ⟨_, ⟨x, mem_ball_zero_iff.2 hx, rfl⟩, hxf⟩
