KuratowskiBasic.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The Kuratowski measure from finite diameter covers

The infimum uses positive real radii. The boundedness hypotheses ensure that its defining set is nonempty. No compactness theorem or fixed-point principle is part of this definition.

def OAI.Tingley.FiniteDiameterCover line 20
Source documentation
A finite family of sets of pairwise diameter at most the given radius.
```
def FiniteDiameterCover (H : Set E) (δ : ℝ) : Prop :=
…
```
theorem OAI.Tingley.FiniteDiameterCover.of_fintype line 28
theorem OAI.Tingley.FiniteDiameterCover.of_finite line 38
theorem OAI.Tingley.FiniteDiameterCover.empty line 45
theorem OAI.Tingley.FiniteDiameterCover.mono_set line 50
theorem OAI.Tingley.FiniteDiameterCover.mono_radius line 55
theorem OAI.Tingley.FiniteDiameterCover.closure line 60
def OAI.Tingley.coverRadii line 71
Source documentation
Positive radii admitting a finite diameter cover.
```
def coverRadii (H : Set E) : Set ℝ :=
…
```
def OAI.Tingley.chi line 75
Source documentation
The Kuratowski measure of noncompactness, on bounded sets.
```
noncomputable def chi (H : Set E) : ℝ := sInf (coverRadii H)
```
Mentions: OAI.Tingley.coverRadii
theorem OAI.Tingley.coverRadii_bddBelow line 77
theorem OAI.Tingley.coverRadii_nonempty line 80
theorem OAI.Tingley.chi_nonneg line 91
theorem OAI.Tingley.chi_le_of_cover line 94
theorem OAI.Tingley.chi_empty line 106
theorem OAI.Tingley.chi_mono line 111
theorem OAI.Tingley.exists_cover_of_chi_lt line 117
theorem OAI.Tingley.chi_closure line 124