Theorems · Theorem · general topology

cauchySeq_of_controlled

∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : SemilatticeSup β] [Nonempty β] (U : β → SetRel α α),
  (∀ s ∈ uniformity α, ∃ n, U n ⊆ s) → ∀ {f : β → α}, (∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N) → CauchySeq f

Defined in

Mathlib.Topology.UniformSpace.Cauchy

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpaceSemilatticeSupNonempty