English
If there exists a bound M with both an upper bound for all x and a lower bound w.r.t. all possible bounds, then the operator norm equals M.
Русский
Если существует предел M, который является верхней границей нормы f на всех x и ниже любой другой допустимой границы, то операторная норма ||f|| равна M.
LaTeX
$$$$ \Big( M \ge 0 \wedge ( \forall x, \|f x\| \le M \|x\| ) \wedge ( \forall N \ge 0, ( \forall x, \|f x\| \le N \|x\| ) \Rightarrow M \le N ) \Big) \Rightarrow \|f\| = M $$$$
Lean4
theorem opNorm_eq_of_bounds {M : ℝ} (M_nonneg : 0 ≤ M) (h_above : ∀ x, ‖f x‖ ≤ M * ‖x‖)
(h_below : ∀ N ≥ 0, (∀ x, ‖f x‖ ≤ N * ‖x‖) → M ≤ N) : ‖f‖ = M :=
le_antisymm (f.opNorm_le_bound M_nonneg h_above)
((le_csInf_iff NormedAddGroupHom.bounds_bddBelow ⟨M, M_nonneg, h_above⟩).mpr fun N ⟨N_nonneg, hN⟩ =>
h_below N N_nonneg hN)
