English
If there is c with ||c|| > 1, then for any nonzero x there exists d ∈ 𝕜 with d ≠ 0 such that ||d x|| < ε, ε/||c|| ≤ ||d x||, and ||d||^{-1} ≤ ε^{-1} ||c|| ||x||.
Русский
Если существует c с ||c|| > 1, то для любого ненулевого x существует d ≠ 0 в 𝕜 such that ||d x|| < ε, ε/||c|| ≤ ||d x||, и ||d||^{-1} ≤ ε^{-1} ||c|| ||x||.
LaTeX
$$$\exists d \in 𝕜, d \neq 0 \wedge \|d \cdot x\| < \varepsilon \wedge (\varepsilon / \|c\| \le \|d \cdot x\|) \wedge (\|d\|^{-1} \le \varepsilon^{-1} \cdot \|c\| \cdot \|x\|).$$$
Lean4
/-- If there is a scalar `c` with `‖c‖>1`, then any element with nonzero norm can be
moved by scalar multiplication to any shell of width `‖c‖`. Also recap information on the norm of
the rescaling element that shows up in applications. -/
theorem rescale_to_shell_semi_normed {c : 𝕜} (hc : 1 < ‖c‖) {ε : ℝ} (εpos : 0 < ε) {x : E} (hx : ‖x‖ ≠ 0) :
∃ d : 𝕜, d ≠ 0 ∧ ‖d • x‖ < ε ∧ (ε / ‖c‖ ≤ ‖d • x‖) ∧ (‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖) :=
(normSeminorm 𝕜 E).rescale_to_shell hc εpos hx
