finite_cover_balls_of_compact — Mathlib

English

A compact subset of a pseudometric space can be covered by finitely many balls of a fixed positive radius.

Русский

Компактное множество в псевдометрическом пространстве можно покрыть конечным числом шаров фиксированного положительного радиуса.

LaTeX

$$$\\exists t\\subseteq s, t\\text{finite} \\land s \\subseteq \\bigcup_{x\\in t} B(x,e)$, где $e>0$$$

Lean4

/-- Any compact set in a pseudometric space can be covered by finitely many balls of a given
positive radius -/
theorem finite_cover_balls_of_compact (hs : IsCompact s) {e : ℝ} (he : 0 < e) :
    ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, ball x e :=
  let ⟨t, hts, ht⟩ := hs.elim_nhds_subcover _ (fun x _ => ball_mem_nhds x he)
  ⟨t, hts, t.finite_toSet, ht⟩

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