English
In a compact space, for a cover by open sets U_i, there exists a neighborhood diameter V such that every point is contained in some ball of radius V lying inside some U_i.
Русский
В компактном пространстве для покрытия открытыми множествами существует диаметр окрестности V, чтобы каждый пункт содержался в шаре радиуса V внутри некоторого U_i.
LaTeX
$$$\exists V \in 𝓤(\alpha), \; \forall x \in K, \exists i, B(x,V) \subseteq U_i$$$
Lean4
theorem lebesgue_number_lemma_nhds {U : α → Set α} (hK : IsCompact K) (hU : ∀ x ∈ K, U x ∈ 𝓝 x) :
∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y, ball x V ⊆ U y :=
by
rcases
lebesgue_number_lemma (U := fun x => interior (U x)) hK (fun _ => isOpen_interior)
(fun x hx => mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x hx)⟩) with
⟨V, V_uni, hV⟩
exact ⟨V, V_uni, fun x hx => (hV x hx).imp fun _ hy => hy.trans interior_subset⟩
