tendsto_closedBall_smallSets — Mathlib

English

In a metric space, for a compact set s and an open cover by sets c_i, there exists δ>0 such that every point of s is contained in some c_i with the ball of radius δ around it contained in that c_i.

Русский

В метрическом пространстве для компактного множества s и открытого покрытия c_i существует δ>0, такое что для каждой точки x∈s существует i с B(x,δ) ⊆ c_i.

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 tendsto_closedBall_smallSets (x : α) : Tendsto (closedBall x) (𝓝 0) (𝓝 x).smallSets :=
  tendsto_smallSets_iff.2 fun _ ↦ eventually_closedBall_subset

Похожие утверждения