English
Every CauSeq in Real with absolute value converges to a constant abs x.
Русский
Каждая кау-секвенция в действительных числах с модулем сходится к константе abs x.
LaTeX
$$$\\exists x, f \\approx \\text{const }|\\cdot|\\ x$$$
Lean4
theorem cauSeq_converges (f : CauSeq ℝ abs) : ∃ x, f ≈ const abs x :=
by
let s := {x : ℝ | const abs x < f}
have lb : ∃ x, x ∈ s := exists_lt f
have ub' : ∀ x, f < const abs x → ∀ y ∈ s, y ≤ x := fun x h y yS => le_of_lt <| const_lt.1 <| CauSeq.lt_trans yS h
have ub : ∃ x, ∀ y ∈ s, y ≤ x := (exists_gt f).imp ub'
refine ⟨sSup s, ((lt_total _ _).resolve_left fun h => ?_).resolve_right fun h => ?_⟩
· rcases h with ⟨ε, ε0, i, ih⟩
refine (csSup_le lb (ub' _ ?_)).not_gt (sub_lt_self _ (half_pos ε0))
refine ⟨_, half_pos ε0, i, fun j ij => ?_⟩
rw [sub_apply, const_apply, sub_right_comm, le_sub_iff_add_le, add_halves]
exact ih _ ij
· rcases h with ⟨ε, ε0, i, ih⟩
refine (le_csSup ub ?_).not_gt ((lt_add_iff_pos_left _).2 (half_pos ε0))
refine ⟨_, half_pos ε0, i, fun j ij => ?_⟩
rw [sub_apply, const_apply, add_comm, ← sub_sub, le_sub_iff_add_le, add_halves]
exact ih _ ij
