English
If s is compact and c is an open cover of s by sets c_i, then there exists δ > 0 such that each point of s is contained in some c_i with the ball of radius δ around it inside c_i.
Русский
Если s компактно и есть открытое покрытие c_i, то существует δ>0, такое что каждая точка s содержится в некотором c_i с шаром радиуса δ вокруг неё внутри c_i.
LaTeX
$$$\text{IsCompact}(s) \rightarrow (\forall i, \ IsOpen(c_i)) \rightarrow s \subseteq \bigcup_i c_i \rightarrow \exists \delta>0, \forall x\in s, \exists i, \mathrm{ball}(x,\delta) \subseteq c_i$$$
Lean4
theorem lebesgue_number_lemma_of_metric {s : Set α} {ι : Sort*} {c : ι → Set α} (hs : IsCompact s)
(hc₁ : ∀ i, IsOpen (c i)) (hc₂ : s ⊆ ⋃ i, c i) : ∃ δ > 0, ∀ x ∈ s, ∃ i, ball x δ ⊆ c i := by
simpa only [ball, UniformSpace.ball, preimage_setOf_eq, dist_comm] using
uniformity_basis_dist.lebesgue_number_lemma hs hc₁ hc₂
