English
Let f be a continuous linear map that satisfies a normalization: there exists x with ‖x‖₊ = 1 and ‖f x‖₊ > r for some r < ‖f‖₊. Then there exists such an x with ‖x‖₊ = 1 attaining the bound away from zero.
Русский
Пусть f — непрерывно линейное отображение, которое удовлетворяет нормализации: существует x с ‖x‖₊ = 1 и ‖f x‖₊ > r для некоторого r < ‖f‖₊. Тогда существует такое x с ‖x‖₊ = 1, достигающее границу.
LaTeX
$$$\\forall f: E \\to SL[σ_{12}] F\\, {r : \\mathbb{R}_{\\ge 0}},\\ (r < \\|f\\|_{+})\\Rightarrow \\exists x:\\,E, \\|x\\|_{+} = 1 \\land r < \\|f x\\|_{+}.$$$
Lean4
theorem exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm [NormedAlgebra ℝ 𝕜] (f : E →SL[σ₁₂] F) {r : ℝ≥0} (hr : r < ‖f‖₊) :
∃ x : E, ‖x‖₊ = 1 ∧ r < ‖f x‖₊ :=
by
obtain ⟨x, hlt, hr⟩ := exists_lt_apply_of_lt_opNNNorm f hr
obtain rfl | hx0 := eq_zero_or_nnnorm_pos x
· simp at hr
use algebraMap ℝ 𝕜 ‖x‖⁻¹ • x
suffices r < ‖x‖₊⁻¹ * ‖f x‖₊ by simpa [nnnorm_smul, inv_mul_cancel₀ hx0.ne'] using this
calc
r < 1⁻¹ * ‖f x‖₊ := by simpa
_ < ‖x‖₊⁻¹ * ‖f x‖₊ := by gcongr; exact (zero_le r).trans_lt hr
