English
Let f be a continuous linear map between normed spaces. If a real number r is strictly less than the operator norm ‖f‖, then there exists a vector x with norm less than 1 such that ‖f x‖ exceeds r. (In particular, if r < 0, taking x = 0 works.)
Русский
Пусть f — непрерывно линейное отображение между нормированными пространствами. Если какое−то число r строго меньше операторной нормы ‖f‖, то существует вектор x такой, что ‖x‖ < 1 и ‖f x‖ > r. (В частности, если r < 0, можно взять x = 0.)
LaTeX
$$$\\forall f: E \\to SL[\\sigma_{12}] F, \\forall r\\in\\mathbb{R},\\ r < \\|f\\| \\,\\Rightarrow \\\\exists x:\\,E,\\ \\|x\\| < 1 \\ \\land\\ r < \\|f x\\|.$$$$
Lean4
theorem exists_lt_apply_of_lt_opNorm (f : E →SL[σ₁₂] F) {r : ℝ} (hr : r < ‖f‖) : ∃ x : E, ‖x‖ < 1 ∧ r < ‖f x‖ :=
by
by_cases hr₀ : r < 0
· exact ⟨0, by simpa using hr₀⟩
· lift r to ℝ≥0 using not_lt.1 hr₀
exact f.exists_lt_apply_of_lt_opNNNorm hr
