countable_closure_of_compact — Mathlib

English

Variant of total boundedness: for every ε > 0 there exists t ⊆ s with t finite such that s ⊆ ⋃ y ∈ t, ball y ε.

Русский

Вариант полной ограниченности: для каждого ε > 0 существует t ⊆ s, конечное, такое что s ⊆ ⋃_{y∈t} B(y, ε).

LaTeX

$$TotallyBounded s ↔ ∀ ε > 0, ∃ t ⊆ s ∧ t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε$$

Lean4

/-- A compact set in an emetric space is separable, i.e., it is the closure of a countable set. -/
theorem countable_closure_of_compact {s : Set γ} (hs : IsCompact s) : ∃ t, t ⊆ s ∧ t.Countable ∧ s = closure t :=
  by
  rcases subset_countable_closure_of_compact hs with ⟨t, hts, htc, hsub⟩
  exact ⟨t, hts, htc, hsub.antisymm (closure_minimal hts hs.isClosed)⟩

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