English
Let K be compact in a uniform space and {U_j} an open cover of K. Then there exists an index i with ball(x, V_i) ⊆ U_j for all x ∈ K for some j dependent on x.
Русский
Пусть K компактно в равномерном пространстве, а {U_j} — открытое покрытие K. Существет индекс i с тем, что окружность Ball(x, V_i) ⊆ U_j для всех x∈K при некотором j зависящем от x.
LaTeX
$$$$\\exists i, p(i) \\wedge \\forall x \\in K, \\exists j, \\mathrm{ball}(x, V_i) \\subseteq U_j.$$$$
Lean4
protected theorem lebesgue_number_lemma_nhds {ι' : Sort*} {p : ι' → Prop} {V : ι' → Set (α × α)} {U : α → Set α}
(hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K) (hU : ∀ x ∈ K, U x ∈ 𝓝 x) :
∃ i, p i ∧ ∀ x ∈ K, ∃ y, ball x (V i) ⊆ U y :=
by
refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhds hK hU)
exact fun s t hst ht x hx ↦ (ht x hx).imp fun y hy ↦ Subset.trans (ball_mono hst _) hy
