English
Let hbasis be a basis for the uniformity on α, and K compact. If U is a family of sets over α with U x hx ∈ nhds x, then there exists an index i from the basis such that for all x in K there is a y in K with ball(x, V_i) ⊆ U(y,y).
Русский
Пусть hbasis задаёт базис для равномерности на α, K компактно. Если U x hx ∈ nhds x, тогда существует индекс i из базиса, такой что для каждого x∈K существует y∈K с ball(x, V_i) ⊆ U(y,y).
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_nhds' {ι' : Sort*} {p : ι' → Prop} {V : ι' → Set (α × α)}
{U : (x : α) → x ∈ K → Set α} (hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K) (hU : ∀ x hx, U x hx ∈ 𝓝 x) :
∃ i, p i ∧ ∀ x ∈ K, ∃ y : K, ball x (V i) ⊆ U y y.2 :=
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
