cauchySeq_tendsto_of_isComplete — Mathlib

English

If K is complete and u(n) ∈ K, and u is Cauchy, then there exists v ∈ K with u converging to v.

Русский

Если K полно и u_n ∈ K, а u — Cauchy, то найдется v ∈ K, к которому сходится u.

LaTeX

$$$\\text{IsComplete}(K) \\rightarrow (\\forall n, u(n) ∈ K) \\rightarrow CauchySeq(u) \\rightarrow \\exists v \\in K, Tendsto u\\ atTop\\ (nhds\\ v)$$$

Lean4

/-- If `K` is a complete subset, then any Cauchy sequence in `K` converges to a point in `K` -/
theorem cauchySeq_tendsto_of_isComplete [Preorder β] {K : Set α} (h₁ : IsComplete K) {u : β → α} (h₂ : ∀ n, u n ∈ K)
    (h₃ : CauchySeq u) : ∃ v ∈ K, Tendsto u atTop (𝓝 v) :=
  h₁ _ h₃ <| le_principal_iff.2 <| mem_map_iff_exists_image.2 ⟨univ, univ_mem, by rwa [image_univ, range_subset_iff]⟩

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