exists_seq_norm_le_one_le_norm_sub

English

There exists a sequence {f_n} in a non-finite-dimensional space with ||f_n|| ≤ R and 1 ≤ ||f_m - f_n|| for m ≠ n.

Русский

Существует последовательность {f_n} в бесконечно-мерном пространстве с ||f_n|| ≤ R и 1 ≤ ||f_m - f_n|| для m ≠ n.

LaTeX

$$$[NotFiniteDimensional 𝕜 E] \\\\Rightarrow ∃ R>0, ∃ f: ℕ \\\\to E, (∀ n, ||f(n)|| ≤ R) ∧ (Pairwise (fun m n => 1 ≤ ||f(m) - f(n)||))$$$

Lean4

theorem exists_seq_norm_le_one_le_norm_sub (h : ¬FiniteDimensional 𝕜 E) :
    ∃ (R : ℝ) (f : ℕ → E), 1 < R ∧ (∀ n, ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖ :=
  by
  obtain ⟨c, hc⟩ : ∃ c : 𝕜, 1 < ‖c‖ := NormedField.exists_one_lt_norm 𝕜
  have A : ‖c‖ < ‖c‖ + 1 := by linarith
  rcases exists_seq_norm_le_one_le_norm_sub' hc A h with ⟨f, hf⟩
  exact ⟨‖c‖ + 1, f, hc.trans A, hf.1, hf.2⟩

Похожие утверждения