exists_mul_lt_of_lt_opNorm — Mathlib

English

For a bounded operator f with ‖f‖₊ > r, there exists x with ‖x‖₊ < 1 and r < ‖f x‖₊.

Русский

Если ‖f‖₊ > r, существует x с ‖x‖₊ < 1 и r < ‖f x‖₊.

LaTeX

$$Exists x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊$$

Lean4

theorem exists_mul_lt_of_lt_opNorm (f : E →SL[σ₁₂] F) {r : ℝ} (hr₀ : 0 ≤ r) (hr : r < ‖f‖) : ∃ x, r * ‖x‖ < ‖f x‖ :=
  by
  lift r to ℝ≥0 using hr₀
  exact f.exists_mul_lt_apply_of_lt_opNNNorm hr

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