English
Let K be compact and S a collection of open sets with K ⊆ ⋃₀ S. Then there exists an entourage V such that for every x ∈ K there is some set s ∈ S with ball(x,V) ⊆ s.
Русский
Пусть K компактно и S — семейство открытых множеств с K ⊆ ⋃₀ S. Тогда существует окружность V, такая что для каждого x∈K ∃ s∈S: ball(x,V) ⊆ s.
LaTeX
$$$$\\exists V \\in 𝓤(\\alpha), \\; \\forall x \\in K, \\exists s \\in S: \\; \\mathrm{ball}(x,V) \\subseteq s.$$$$
Lean4
/-- Let `c : Set (Set α)` be an open cover of a compact set `s`. Then there exists an entourage
`n` such that for each `x ∈ s` its `n`-neighborhood is contained in some `t ∈ c`. -/
theorem lebesgue_number_lemma_sUnion {S : Set (Set α)} (hK : IsCompact K) (hopen : ∀ s ∈ S, IsOpen s)
(hcover : K ⊆ ⋃₀ S) : ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ s ∈ S, ball x V ⊆ s :=
by
rw [sUnion_eq_iUnion] at hcover
simpa using lebesgue_number_lemma hK (by simpa) hcover
