cauchySeq_tendsto_of_complete — Mathlib

English

A Cauchy sequence in a complete space converges.

Русский

Cauchy-последовательность в полном пространстве сходится.

LaTeX

$$$\\text{CauchySeq}(u) \\rightarrow \\exists x, Tendsto u\\ (atTop)\\ (nhds\\ x)$$$

Lean4

/-- A Cauchy sequence in a complete space converges -/
theorem cauchySeq_tendsto_of_complete [Preorder β] [CompleteSpace α] {u : β → α} (H : CauchySeq u) :
    ∃ x, Tendsto u atTop (𝓝 x) :=
  CompleteSpace.complete H

Похожие утверждения