Theorems · Definition · general topology

UniformCauchySeqOnFilter

{α : Type u_1} → {β : Type u_2} → {ι : Type u_4} → [UniformSpace β] → (ι → α → β) → Filter ι → Filter α → Prop

A sequence is uniformly Cauchy if eventually all of its pairwise differences are uniformly bounded

Defined in

Mathlib.Topology.UniformSpace.UniformConvergence

Cited by

14 results in Mathlib

Foundations

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

Assumes

UniformSpace