English
If x is an upper bound for a tail of a Cauchy sequence f, then x is an upper bound for the real mk(f).
Русский
Если x является верхней границей хвоста последовательности Коши f, то x является верхней границей Real.mk(f).
LaTeX
$$$\bigl(\exists i \in \mathbb{N}, \forall j \ge i,\ x \le f_j\bigr) \Rightarrow x \le \operatorname{mk}(f)$$$
Lean4
theorem le_mk_of_forall_le {f : CauSeq ℚ abs} : (∃ i, ∀ j ≥ i, x ≤ f j) → x ≤ mk f :=
by
intro h
induction x using Real.ind_mk
apply le_of_not_gt
rw [mk_lt]
rintro ⟨K, K0, hK⟩
obtain ⟨i, H⟩ := exists_forall_ge_and h (exists_forall_ge_and hK (f.cauchy₃ <| half_pos K0))
apply not_lt_of_ge (H _ le_rfl).1
rw [← mk_const, mk_lt]
refine ⟨_, half_pos K0, i, fun j ij => ?_⟩
have := add_le_add (H _ ij).2.1 (le_of_lt (abs_lt.1 <| (H _ le_rfl).2.2 _ ij).1)
rwa [← sub_eq_add_neg, sub_self_div_two, sub_apply, sub_add_sub_cancel] at this
