English
If a normed field β is complete with respect to Cau_seq.IsComplete (i.e., Cauchy sequences converge), then β is a complete metric space.
Русский
Если нормированное поле β полно относительно последовательностей Кауса (CauSeq), то β является полным метрическим пространством.
LaTeX
$$$\operatorname{CauSeq.IsComplete}(\beta,\|\cdot\|) \Rightarrow \operatorname{CompleteSpace}\beta$$$
Lean4
/-- A complete normed field is complete as a metric space, as Cauchy sequences converge by
assumption and this suffices to characterize completeness. -/
instance (priority := 100) completeSpace_of_cauSeq_isComplete [CauSeq.IsComplete β norm] : CompleteSpace β :=
by
apply complete_of_cauchySeq_tendsto
intro u hu
have C : IsCauSeq norm u := isCauSeq_iff_cauchySeq.2 hu
exists CauSeq.lim ⟨u, C⟩
rw [Metric.tendsto_atTop]
intro ε εpos
obtain ⟨N, hN⟩ := (CauSeq.equiv_lim ⟨u, C⟩) _ εpos
exists N
simpa [dist_eq_norm] using hN
