Theorems · Theorem · general topology

Filter.HasBasis.cauchySeq_iff

∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Sort u_1} [Nonempty β] [inst : SemilatticeSup β]
  {u : β → α} {p : γ → Prop} {s : γ → SetRel α α},
  (uniformity α).HasBasis p s →
    (CauchySeq u ↔ ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i)

Defined in

Mathlib.Topology.UniformSpace.Cauchy

Cited by

5 results in Mathlib

Foundations

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

Assumes

UniformSpaceNonemptySemilatticeSup