English
Let p, q be seminorms on a normed space E over 𝕜. Suppose ε > 0, C ≥ 0, and c ∈ 𝕜 with 1 < ||c||. If for all x we have ε/||c|| ≤ p(x) and p(x) < ε implies q(x) ≤ (C · p)(x), then for every x with p(x) ≠ 0 we also have q(x) ≤ (C · p)(x).
Русский
Пусть p, q — семинормы на нормированном пространстве E над 𝕜. Пусть ε > 0, C ≥ 0 и c ∈ 𝕜 с 1 < ||c||. Если для всех x выполняется неравенство ε/||c|| ≤ p(x) и p(x) < ε, тогда q(x) ≤ (C · p)(x); тогда для любого x с p(x) ≠ 0 выполняется q(x) ≤ (C · p)(x).
LaTeX
$$$\forall p,q : \mathrm{Seminorm}_{\mathbb{k}}(E),\ \forall \varepsilon > 0,\ \forall C \in \mathbb{R}_{\ge 0},\ \forall c \in 𝕜,\ (1 < \|c\|) \Rightarrow\ (\forall x \in E,\ \varepsilon / \|c\| \le p(x) \land p(x) < \varepsilon \Rightarrow q(x) \le (C \cdot p)(x)) \Rightarrow (\forall x \in E,\ p(x) \neq 0 \Rightarrow q(x) \le (C \cdot p)(x)).$$$
Lean4
/-- A version of `Seminorm.bound_of_shell` expressed using pointwise scalar multiplication of
seminorms. -/
theorem bound_of_shell_smul (p q : Seminorm 𝕜 E) {ε : ℝ} {C : ℝ≥0} (ε_pos : 0 < ε) {c : 𝕜} (hc : 1 < ‖c‖)
(hf : ∀ x, ε / ‖c‖ ≤ p x → p x < ε → q x ≤ (C • p) x) {x : E} (hx : p x ≠ 0) : q x ≤ (C • p) x :=
Seminorm.bound_of_shell p q ε_pos hc hf hx
