finite_approx_of_totallyBounded — Mathlib

English

If s is totally bounded, then for each ε>0 there exists a finite subset t such that s is covered by ε-balls around t.

Русский

Если s полностью ограничено, то для каждого ε>0 существует конечное подмножество t такое, что s покрыто шариками B(y,ε) вокруг точек t.

LaTeX

$$$\\forall ε>0, \\exists t \\subseteq s, t\\text{ finite}, s \\subseteq \\bigcup_{y\\in t} B(y, ε)$$$

Lean4

theorem finite_approx_of_totallyBounded {s : Set α} (hs : TotallyBounded s) :
    ∀ ε > 0, ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ y ∈ t, ball y ε :=
  by
  intro ε ε_pos
  rw [totallyBounded_iff_subset] at hs
  exact hs _ (dist_mem_uniformity ε_pos)

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