English
The neighborhoods of a compact set K form a basis consisting of unions of balls around points of K.
Русский
Окрестности множества K образуют базис из объединений шаров вокруг точек K.
LaTeX
$$$$ (\\mathcal{N}^\\# K).HasBasis p \\; (i \\mapsto \\bigcup_{x \\in K} \\mathrm{ball}(x, V_i)). $$$$
Lean4
/-- 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`. -/
theorem nhdsSet_basis_uniformity {p : ι → Prop} {V : ι → Set (α × α)} (hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K) :
(𝓝ˢ K).HasBasis p fun i => ⋃ x ∈ K, ball x (V i) where
mem_iff'
U := by
constructor
· intro H
have HKU : K ⊆ ⋃ _ : Unit, interior U := by simpa only [iUnion_const, subset_interior_iff_mem_nhdsSet] using H
obtain ⟨i, hpi, hi⟩ : ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ interior U := by
simpa using hbasis.lebesgue_number_lemma hK (fun _ ↦ isOpen_interior) HKU
exact ⟨i, hpi, hi.trans interior_subset⟩
· rintro ⟨i, hpi, hi⟩
refine mem_of_superset (bUnion_mem_nhdsSet fun x _ ↦ ?_) hi
exact ball_mem_nhds _ <| hbasis.mem_of_mem hpi
