Theorems · Theorem · general topology

Filter.HasBasis.lebesgue_number_lemma_nhdsWithin

∀ {α : Type ua} [inst : UniformSpace α] {K : Set α} {ι' : Sort u_2} {p : ι' → Prop} {V : ι' → Set (α × α)}
  {U : α → Set α},
  (uniformity α).HasBasis p V →
    IsCompact K → (∀ x ∈ K, U x ∈ nhdsWithin x K) → ∃ i, p i ∧ ∀ x ∈ K, ∃ y, UniformSpace.ball x (V i) ∩ K ⊆ U y

Defined in

Mathlib.Topology.UniformSpace.Compact

Cited by

1 results in Mathlib

Foundations

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

Assumes

UniformSpace