KuratowskiNested.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Nested sets with vanishing Kuratowski measure

Small finite diameter covers make the range of a selected sequence totally bounded. Its compact closure supplies a point in all the nested closed sets. The whole intersection is compact by its own arbitrarily fine finite covers.

theorem OAI.Tingley.nonempty_isCompact_iInter_of_finiteDiameterCover line 30

Source documentation

A nested sequence with arbitrarily fine finite diameter covers has a nonempty compact intersection. No original member is assumed compact.

theorem nonempty_isCompact_iInter_of_finiteDiameterCover
    (C : ℕ → Set E) (hanti : Antitone C)
    (hne : ∀ n, (C n).Nonempty)
    (hclosed : ∀ n, IsClosed (C n))
    (hsmall : ∀ ε : ℝ, 0 < ε →
      ∃ N : ℕ, FiniteDiameterCover (C N) ε) :
    (⋂ n, C n).Nonempty ∧ IsCompact (⋂ n, C n) := by
…

Mentions: OAI.Tingley.FiniteDiameterCover

theorem OAI.Tingley.nonempty_isCompact_iInter_of_chi_tendsto_zero line 80
Source documentation
A decreasing sequence of nonempty closed sets in a complete metric space has a nonempty compact intersection when its Kuratowski measures tend to zero. Boundedness of the first set supplies boundedness at every later index.
```
theorem nonempty_isCompact_iInter_of_chi_tendsto_zero
    (C : ℕ → Set E)
    (hanti : Antitone C)
    (hne : ∀ n, (C n).Nonempty)
    (hclosed : ∀ n, IsClosed (C n))
    (hbound : Bornology.IsBounded (C 0))
    (hchi : Tendsto (fun n => chi (C n)) atTop (𝓝 0)) :
    (⋂ n, C n).Nonempty ∧ IsCompact (⋂ n, C n) := by
…
```
Mentions: OAI.Tingley.chi