English
In an infinite-dimensional normed space, there exists a sequence with all elements bounded by R and pairwise distance at least 1.
Русский
В бесконечно-мерном нормированном пространстве существует последовательность {f_n} с ||f_n|| ≤ R и ||f_m - f_n|| ≥ 1 при m ≠ n.
LaTeX
$$$[NotFiniteDimensional 𝕜 E] \\\\Rightarrow ∃ f: ℕ \\\\to E, (∀ n, ||f(n)|| ≤ R) ∧ (Pairwise (fun m n => 1 ≤ ||f(m) - f(n)||))$$$
Lean4
/-- In an infinite-dimensional normed space, there exists a sequence of points which are all
bounded by `R` and at distance at least `1`. For a version not assuming `c` and `R`, see
`exists_seq_norm_le_one_le_norm_sub`. -/
theorem exists_seq_norm_le_one_le_norm_sub' {c : 𝕜} (hc : 1 < ‖c‖) {R : ℝ} (hR : ‖c‖ < R) (h : ¬FiniteDimensional 𝕜 E) :
∃ f : ℕ → E, (∀ n, ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖ :=
by
have : IsSymm E fun x y : E => 1 ≤ ‖x - y‖ := by
constructor
intro x y hxy
rw [← norm_neg]
simpa
apply exists_seq_of_forall_finset_exists' (fun x : E => ‖x‖ ≤ R) fun (x : E) (y : E) => 1 ≤ ‖x - y‖
rintro s -
exact exists_norm_le_le_norm_sub_of_finset hc hR h s
