exists_mul_lt_apply_of_lt_opNNNorm

English

If r is strictly less than the NN-norm of f, there exists x with ‖x‖₊ < 1 such that r < ‖f x‖₊.

Русский

Если r меньше чем ‖f‖₊, найдётся x с ‖x‖₊ < 1 и r < ‖f x‖₊.

LaTeX

$$Exists x, with ‖x‖₊ < 1 and r < ‖f x‖₊$$

Lean4

theorem exists_mul_lt_apply_of_lt_opNNNorm (f : E →SL[σ₁₂] F) {r : ℝ≥0} (hr : r < ‖f‖₊) : ∃ x, r * ‖x‖₊ < ‖f x‖₊ := by
  simpa only [not_forall, not_le, Set.mem_setOf] using
    notMem_of_lt_csInf (nnnorm_def f ▸ hr : r < sInf {c : ℝ≥0 | ∀ x, ‖f x‖₊ ≤ c * ‖x‖₊}) (OrderBot.bddBelow _)

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