Theorems · Theorem · general topology

lebesgue_number_lemma_nhds

∀ {α : Type ua} [inst : UniformSpace α] {K : Set α} {U : α → Set α},
  IsCompact K → (∀ x ∈ K, U x ∈ nhds x) → ∃ V ∈ uniformity α, ∀ x ∈ K, ∃ y, UniformSpace.ball x V ⊆ U y

Defined in

Mathlib.Topology.UniformSpace.Compact

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpace