English
Let E be a nontrivial normed space over a nontrivial normed field 𝕜. Then for every real number c, there exists x in E with ∥x∥ > c.
Русский
Пусть E — ненулевое нормированное пространство над ненулевой нормированной полем 𝕜. Тогда для каждого числа c ∈ ℝ существует x ∈ E такое, что ∥x∥ > c.
LaTeX
$$$\\\\forall c \\\\in \\\\mathbb{R}, \\\\exists x \\\\in E, \\\\|x\\\\| > c$$$
Lean4
/-- If `E` is a nontrivial normed space over a nontrivially normed field `𝕜`, then `E` is unbounded:
for any `c : ℝ`, there exists a vector `x : E` with norm strictly greater than `c`. -/
theorem exists_lt_norm (c : ℝ) : ∃ x : E, c < ‖x‖ :=
by
rcases exists_ne (0 : E) with ⟨x, hx⟩
rcases NormedField.exists_lt_norm 𝕜 (c / ‖x‖) with ⟨r, hr⟩
use r • x
rwa [norm_smul, ← div_lt_iff₀]
rwa [norm_pos_iff]
