bound_of_shell_semi_normed — Mathlib

English

Under shell bounds, a global norm bound is deduced for a semilinear map.

Русский

При ограничении оболочки выводится глобальное ограничение нормы линейного отображения.

LaTeX

$$$\exists C: \mathbb{R}_{\ge 0},\forall x\neq 0, \|f x\| ≤ C \|x\|$$$

Lean4

theorem bound_of_shell_semi_normed [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕) {ε C : ℝ} (ε_pos : 0 < ε) {c : 𝕜}
    (hc : 1 < ‖c‖) (hf : ∀ x, ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) {x : E} (hx : ‖x‖ ≠ 0) : ‖f x‖ ≤ C * ‖x‖ :=
  (normSeminorm 𝕜 E).bound_of_shell ((normSeminorm 𝕜₂ F).comp ⟨⟨f, map_add f⟩, map_smulₛₗ f⟩) ε_pos hc hf hx

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