opNorm_le_of_nhds_zero — Mathlib

English

If ∥f x∥ ≤ C ∥x∥ holds eventually near 0, then ‖f‖ ≤ C.

Русский

Если неравенство ∥f x∥ ≤ C ∥x∥ верно в окрестности 0 за пределами, то ‖f‖ ≤ C.

LaTeX

$$$\\|f\\| \\le C$ if $f x$ is bounded by C∥x∥ in a neighborhood of 0$$

Lean4

theorem opNorm_le_of_nhds_zero {f : E →SL[σ₁₂] F} {C : ℝ} (hC : 0 ≤ C) (hf : ∀ᶠ x in 𝓝 (0 : E), ‖f x‖ ≤ C * ‖x‖) :
    ‖f‖ ≤ C :=
  let ⟨_, ε0, hε⟩ := Metric.eventually_nhds_iff_ball.1 hf
  opNorm_le_of_ball ε0 hC hε

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