Theorems · Theorem · general topology

isCompact_closure_interUnionBalls

∀ {α : Type u} [uniformSpace : UniformSpace α] {p : ℕ → Prop} {U : ℕ → SetRel α α},
  (uniformity α).HasBasis p U →
    ∀ [CompleteSpace α] (xs : ℕ → α) (u : ℕ → ℕ), IsCompact (closure (interUnionBalls xs u U))

The construction interUnionBalls is used to have a relatively compact set.

Defined in

Mathlib.Topology.UniformSpace.Cauchy

Cited by

1 results in Mathlib

Foundations

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

Assumes

UniformSpaceCompleteSpace