English
Given an open basis in a compact set K, for any open U and neighborhood structure restricted to K, there exists i such that balls of radius V_i around points of K form subsets of U(y) for some y ∈ K.
Русский
Для компактного K и открытого базиса в K существует i, что окрестностиBall(x,V_i) для x∈K лежат внутри U(y) для некоторых y∈K.
LaTeX
$$$$\\exists i, p(i) \\wedge \\forall x \\in K, \\exists y \\in K: B(x,V_i) \\subseteq U(y,y).$$$$
Lean4
protected theorem lebesgue_number_lemma_nhdsWithin' {ι' : Sort*} {p : ι' → Prop} {V : ι' → Set (α × α)}
{U : (x : α) → x ∈ K → Set α} (hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K) (hU : ∀ x hx, U x hx ∈ 𝓝[K] x) :
∃ i, p i ∧ ∀ x ∈ K, ∃ y : K, ball x (V i) ∩ K ⊆ U y y.2 :=
by
refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhdsWithin' hK hU)
exact fun s t hst ht x hx ↦ (ht x hx).imp fun y hy ↦ Subset.trans (Set.inter_subset_inter_left K (ball_mono hst _)) hy
