English
If f: ℕ → ℚ is a rational-valued sequence approaching x ∈ ℝ (i.e., for every ε>0 there is i such that for all j≥i, |f(j)−x|<ε), then there exists a witness h' such that the real constructed from f represents x; i.e., x is represented by the Cauchy sequence f of rationals.
Русский
Если f: ℕ → ℚ является последовательностью рациональных чисел, сходящейся к x ∈ ℝ, то существует ядро h' такое, что созданное на основе f вещественное число совпадает с x; то есть x имеет представление как предел последовательности рациональных.
LaTeX
$$$\exists f:\mathbb{N}\to \mathbb{Q},\; \forall \epsilon>0,\; \exists i,\forall j\ge i,|f(j)-x|<\epsilon \;\Rightarrow\; \exists h'\, (\text{Real.mk} \langle f,h'\rangle = x)$$$
Lean4
theorem of_near (f : ℕ → ℚ) (x : ℝ) (h : ∀ ε > 0, ∃ i, ∀ j ≥ i, |(f j : ℝ) - x| < ε) : ∃ h', Real.mk ⟨f, h'⟩ = x :=
⟨isCauSeq_iff_lift.2 (CauSeq.of_near _ (const abs x) h),
sub_eq_zero.1 <|
abs_eq_zero.1 <|
(eq_of_le_of_forall_lt_imp_le_of_dense (abs_nonneg _)) fun _ε ε0 =>
mk_near_of_forall_near <| (h _ ε0).imp fun _i h j ij => le_of_lt (h j ij)⟩
