complete_of_cauchySeq_tendsto — Mathlib

English

Same completeness criterion stated via an assumption that Cauchy sequences converge.

Русский

Те же условия полноты выражены через требование, что все последовательности Коши сходятся.

LaTeX

$$$\text{CompleteSpace}(\alpha)$ follows from the stated Cauchy-to-convergent assumption.$$

Lean4

/-- A sequentially complete pseudoemetric space is complete. -/
theorem complete_of_cauchySeq_tendsto : (∀ u : ℕ → α, CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)) → CompleteSpace α :=
  UniformSpace.complete_of_cauchySeq_tendsto

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