English
If a σ-linear map f is locally bounded on a shell around the origin, then there exists a global bound: ∥f x∥ ≤ C ∥x∥ for all x, with some constant C.
Русский
Если отображение f ограничено на оболочке вокруг нуля, то существует глобочная граница: ∥f(x)∥ ≤ C ∥x∥ для всех x.
LaTeX
$$$\\exists C\\ \\forall x:\\, E,\\; \\|f x\\| \\le C \\|x\\|.\\;$ При предположении существования оболочки и константы bound внутри оболочки.$$
Lean4
theorem bound_of_shell [RingHomIsometric σ₁₂] (f : E →ₛₗ[σ₁₂] F) {ε C : ℝ} (ε_pos : 0 < ε) {c : 𝕜} (hc : 1 < ‖c‖)
(hf : ∀ x, ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) (x : E) : ‖f x‖ ≤ C * ‖x‖ :=
by
by_cases hx : x = 0; · simp [hx]
exact SemilinearMapClass.bound_of_shell_semi_normed f ε_pos hc hf (norm_ne_zero_iff.2 hx)
