English
In a normed field, CauSeq is equivalent to the usual notion of Cauchy sequences: IsCauSeq(norm, u) if and only if CauchySeq u.
Русский
В нормированном поле CauSeq эквивалентно обычной концепции последовательности Коши: IsCauSeq(norm, u) тогда и только тогда, когда CauchySeq u.
LaTeX
$$$ IsCauSeq(norm, u) \iff CauchySeq(u). $$$
Lean4
theorem cauchySeq (f : CauSeq β norm) : CauchySeq f :=
by
refine cauchy_iff.2 ⟨by infer_instance, fun s hs => ?_⟩
rcases mem_uniformity_dist.1 hs with ⟨ε, ⟨hε, hεs⟩⟩
obtain ⟨N, hN⟩ := CauSeq.cauchy₂ f hε
exists {n | n ≥ N}.image f
simp only [mem_atTop_sets, mem_map]
constructor
· exists N
intro b hb
exists b
· rintro ⟨a, b⟩ ⟨⟨a', ⟨ha'1, ha'2⟩⟩, ⟨b', ⟨hb'1, hb'2⟩⟩⟩
dsimp at ha'1 ha'2 hb'1 hb'2
rw [← ha'2, ← hb'2]
apply hεs
rw [dist_eq_norm]
apply hN <;> assumption
