Theorems · Theorem · general topology

Filter.HasBasis.totallyBounded_iff

∀ {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {U : ι → SetRel α α},
  (uniformity α).HasBasis p U →
    ∀ {s : Set α}, TotallyBounded s ↔ ∀ (i : ι), p i → ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}

Defined in

Mathlib.Topology.UniformSpace.Cauchy

Cited by

7 results in Mathlib

Foundations

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

Assumes

UniformSpace