Theorems · Theorem · general topology

TotallyBounded.exists_subset

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

Defined in

Mathlib.Topology.UniformSpace.Cauchy

Cited by

1 results in Mathlib

Foundations

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

Assumes

UniformSpace