Theorems · Theorem · general topology

totallyBounded_iff_subset

∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α},
  TotallyBounded s ↔ ∀ d ∈ uniformity α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}

Defined in

Mathlib.Topology.UniformSpace.Cauchy

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpace