English
Let K be a compact subset of a uniform space X. If, for every x in K, the set U(x) is a neighborhood of x within K, then there exists an entourage V such that for every x in K there is some y with ball(x, V) ∩ K ⊆ U(y).
Русский
Пусть K — компактное подмножество равномерного пространства X. Если для каждого x∈K выполнено, что U(x) является окрестностью x внутри K, то существует окружность V such that для каждого x∈K найдется y с ball(x, V) ∩ K ⊆ U(y).
LaTeX
$$$$\\exists V \\in \\mathcal{U}(\\alpha), \\ \\forall x \\in K, \\exists y \\in \\alpha: \\; B(x,V) \\cap K \\subseteq U(y).$$$$
Lean4
theorem lebesgue_number_lemma_nhdsWithin {U : α → Set α} (hK : IsCompact K) (hU : ∀ x ∈ K, U x ∈ 𝓝[K] x) :
∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y, ball x V ∩ K ⊆ U y :=
(lebesgue_number_lemma_nhds hK (fun x hx => Filter.mem_inf_principal'.1 (hU x hx))).imp fun _ ⟨V_uni, hV⟩ =>
⟨V_uni, fun x hx => (hV x hx).imp fun _ hy => (inter_subset _ _ _).2 hy⟩
