totallyBounded_iff — Mathlib

English

A subset s of a pseudo metric space is totally bounded iff for every ε>0 there exists a finite set t such that s is contained in the union of ε-balls centered at points of t.

Русский

Подмножество s псевдометрического пространства полностью ограничено, если для любого ε>0 существует конечное множество точек t, для которых s ⊆ ⋃_{y∈t} B(y,ε).

LaTeX

$$$\\text{TotallyBounded}(s) \\iff \\forall ε>0, \\exists t, t.Finite ∧ s \\subseteq \\bigcup_{y\\in t} B(y, ε)$$$

Lean4

theorem totallyBounded_iff {s : Set α} : TotallyBounded s ↔ ∀ ε > 0, ∃ t : Set α, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε :=
  uniformity_basis_dist.totallyBounded_iff

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