Theorems · Definition · general topology

CauchySeq

{α : Type u} → {β : Type v} → [uniformSpace : UniformSpace α] → [Preorder β] → (β → α) → Prop

Cauchy sequences. Usually defined on ℕ, but often it is also useful to say that a function defined on ℝ is Cauchy at +∞ to deduce convergence. Therefore, we define it in a type class that is general enough to cover both ℕ and ℝ, which are the main motivating examples.

Defined in

Mathlib.Topology.UniformSpace.Cauchy

Cited by

131 results in Mathlib

Foundations

Depth 61 from the axioms, rests on 685 definitions · uses propext, Classical.choice, Quot.sound

Assumes

UniformSpacePreorder