English
In a metric space, for a compact set s and an open cover by sets c which cover s, there exists δ>0 such that every point of s lies in some c and ball around it of radius δ is contained in that c.
Русский
В метрическом пространстве для компактного s и открытого покрытия c покрывающего s существует δ>0, такое что для каждой точки x∈s существует множество c из покрытия с B(x,δ) ⊆ c.
LaTeX
$$$\text{IsCompact}(s)\ \wedge\ (\forall i,\ IsOpen(c_i))\ \wedge\ 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 eventually_isCompact_closedBall [WeaklyLocallyCompactSpace α] (x : α) :
∀ᶠ r in 𝓝 (0 : ℝ), IsCompact (closedBall x r) :=
by
rcases exists_compact_mem_nhds x with ⟨s, s_compact, hs⟩
filter_upwards [eventually_closedBall_subset hs] with r hr
exact IsCompact.of_isClosed_subset s_compact isClosed_closedBall hr
