Theorems · Theorem · general topology

Filter.HasBasis.cauchy_iff

∀ {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {s : ι → SetRel α α},
  (uniformity α).HasBasis p s →
    ∀ {f : Filter α}, Cauchy f ↔ f.NeBot ∧ ∀ (i : ι), p i → ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s i

Defined in

Mathlib.Topology.UniformSpace.Cauchy

Cited by

3 results in Mathlib

Foundations

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

Assumes

UniformSpace