totallyBounded_iff' — Mathlib

English

TotallyBounded s is equivalent to: for every ε > 0, there exists a subset t ⊆ s such that t is finite and s ⊆ ⋃ y ∈ t Ball(y, ε).

Русский

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

LaTeX

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

Lean4

theorem totallyBounded_iff' {s : Set α} :
    TotallyBounded s ↔ ∀ ε > 0, ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ y ∈ t, ball y ε :=
  ⟨fun H _ε ε0 => (totallyBounded_iff_subset.1 H) _ (edist_mem_uniformity ε0), fun H _r ru =>
    let ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 ru
    let ⟨t, _, ft, h⟩ := H ε ε0
    ⟨t, ft, h.trans <| iUnion₂_mono fun _ _ _ => hε⟩⟩

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