Theorems · Theorem · general topology

IsCompact.nhdsSet_basis_uniformity

∀ {α : Type ua} {ι : Sort u_1} [inst : UniformSpace α] {K : Set α} {p : ι → Prop} {V : ι → Set (α × α)},
  (uniformity α).HasBasis p V → IsCompact K → (nhdsSet K).HasBasis p fun i => ⋃ x ∈ K, UniformSpace.ball x (V i)

If K is a compact set in a uniform space and {V i | p i} is a basis of entourages, then {⋃ x ∈ K, UniformSpace.ball x (V i) | p i} is a basis of 𝓝ˢ K. Here "{s i | p i} is a basis of a filter l" means Filter.HasBasis l p s.

Defined in

Mathlib.Topology.UniformSpace.Compact

Cited by

4 results in Mathlib

Foundations

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

Assumes

UniformSpace