Theorems · Theorem · general topology

cauchySeq_tendsto_of_isComplete

∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : Preorder β] {K : Set α},
  IsComplete K → ∀ {u : β → α}, (∀ (n : β), u n ∈ K) → CauchySeq u → ∃ v ∈ K, Filter.Tendsto u Filter.atTop (nhds v)

If K is a complete subset, then any Cauchy sequence in K converges to a point in K

Defined in

Mathlib.Topology.UniformSpace.Cauchy

Cited by

5 results in Mathlib

Foundations

Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

UniformSpacePreorder