English
If there exists c with ||c|| > 1, then for any nonzero x there exists d ∈ 𝕜 such that ||d x|| < ε, ε/||c|| ≤ ||d x||, and ||d||^{-1} ≤ ε^{-1} ||c|| ||x||.
Русский
Если существует c с ||c|| > 1, то для любого ненулевого x существует d ∈ 𝕜 такое, что ||d x|| < ε, ε/||c|| ≤ ||d x||, и ||d||^{-1} ≤ ε^{-1} ||c|| ||x||.
LaTeX
$$$\exists d \in 𝕜, d \neq 0 ∧ \|d \cdot x\| < \varepsilon ∧ (\varepsilon / \|c\| ≤ \|d \cdot x\|) ∧ (\|d\|^{-1} ≤ \varepsilon^{-1} \cdot \|c\| \cdot \|x\|).$$$
Lean4
/-- If there is a scalar `c` with `‖c‖>1`, then any element 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 [NormedAddCommGroup F] [NormedSpace 𝕜 F] {c : 𝕜} (hc : 1 < ‖c‖) {ε : ℝ} (εpos : 0 < ε) {x : F}
(hx : x ≠ 0) : ∃ d : 𝕜, d ≠ 0 ∧ ‖d • x‖ < ε ∧ (ε / ‖c‖ ≤ ‖d • x‖) ∧ (‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖) :=
rescale_to_shell_semi_normed hc εpos (norm_ne_zero_iff.mpr hx)
