opNorm_le_of_ball — Mathlib

English

A refined shell-based bound: under certain shell constraints, ‖f‖ ≤ C.

Русский

Уточненная оболочечная граница: при данных условиях оболочки ‖f‖ ≤ C.

LaTeX

$$$\\|f\\| ≤ C$ under shell-type constraints$$

Lean4

theorem opNorm_le_of_ball {f : E →SL[σ₁₂] F} {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C)
    (hf : ∀ x ∈ ball (0 : E) ε, ‖f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ C :=
  by
  rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
  refine opNorm_le_of_shell ε_pos hC hc fun x _ hx => hf x ?_
  rwa [ball_zero_eq]

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