KuratowskiTotalBounded.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite diameter covers and total boundedness

The Kuratowski cover predicate is equivalent to arbitrarily fine finite metric covers. Its zero value characterizes total boundedness on bounded sets. A selected point from each member of a nested family has totally bounded range when sufficiently late members admit arbitrarily fine diameter covers.

theorem OAI.Tingley.totallyBounded_iff_finiteDiameterCover line 30
Source documentation
Total boundedness is equivalent to finite pairwise-diameter covers at every positive scale. No completeness or nonemptiness hypothesis is needed.
```
theorem totallyBounded_iff_finiteDiameterCover {H : Set E} :
    TotallyBounded H ↔ ∀ ε : ℝ, 0 < ε → FiniteDiameterCover H ε := by
…
```
Mentions: OAI.Tingley.FiniteDiameterCover
theorem OAI.Tingley.chi_eq_zero_iff_totallyBounded line 73
Source documentation
On bounded sets, vanishing Kuratowski measure is exactly total boundedness. The boundedness premise ensures that the real infimum defining chi has genuine admissible cover radii.
```
theorem chi_eq_zero_iff_totallyBounded {H : Set E}
    (hH : Bornology.IsBounded H) : chi H = 0 ↔ TotallyBounded H := by
…
```
Mentions: OAI.Tingley.chi
theorem OAI.Tingley.totallyBounded_range_of_nested_finiteDiameterCover line 97
Source documentation
Cover the entire selected range by finitely many prefix singletons and a small cover of a sufficiently late member. The cutoff may depend on the scale; no fixed member of the original family is assumed totally bounded.
```
theorem totallyBounded_range_of_nested_finiteDiameterCover
    (C : ℕ → Set E) (hanti : Antitone C)
    (x : ℕ → E) (hx : ∀ n, x n ∈ C n)
    (hsmall : ∀ ε : ℝ, 0 < ε →
      ∃ N : ℕ, FiniteDiameterCover (C N) ε) :
    TotallyBounded (Set.range x) := by
…
```
Mentions: OAI.Tingley.FiniteDiameterCover