English
Let {U_i} be an open cover of a compact set K and suppose the uniform structure has a basis {V_i}. Then there is some index i such that for every x in K there exists j with ball(x, V_i) ⊆ U_j.
Русский
Пусть {U_i} — открытое покрытие компактного множества K и имеется база окружностей {V_i} для uniformity. Тогда существует индекс i such that для каждого x∈K найдется j с.ball(x, V_i) ⊆ U_j.
LaTeX
$$$$\\exists i, p(i) \\wedge \\forall x \\in K, \\exists j, \\mathrm{ball}(x, V_i) \\subseteq U_j.$$$$
Lean4
/-- Let `U : ι → Set α` be an open cover of a compact set `K`.
Then there exists an entourage `V`
such that for each `x ∈ K` its `V`-neighborhood is included in some `U i`.
Moreover, one can choose an entourage from a given basis. -/
protected theorem lebesgue_number_lemma {ι' ι : Sort*} {p : ι' → Prop} {V : ι' → Set (α × α)} {U : ι → Set α}
(hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K) (hopen : ∀ j, IsOpen (U j)) (hcover : K ⊆ ⋃ j, U j) :
∃ i, p i ∧ ∀ x ∈ K, ∃ j, ball x (V i) ⊆ U j :=
by
refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma hK hopen hcover)
exact fun s t hst ht x hx ↦ (ht x hx).imp fun i hi ↦ Subset.trans (ball_mono hst _) hi
