Theorems · Theorem · general topology

isComplete_iff_ultrafilter

∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α},
  IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ Filter.principal s → ∃ x ∈ s, ↑l ≤ nhds x

Defined in

Mathlib.Topology.UniformSpace.Cauchy

Cited by

1 results in Mathlib

Foundations

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

Assumes

UniformSpace