isCompact_closure_of_totallyBounded_quasiComplete

English

If s is totally bounded and the ambient space is quasi-complete, then closure(s) is compact.

Русский

Если s тотально ограничено, а окружающее пространство квази-полное, то замыкание s компактно.

LaTeX

$$$\\text{TotallyBounded}(s) \\Rightarrow \\operatorname{IsCompact}(\\overline{s})$ (in a quasi-complete ambient space)$$

Lean4

/-- [Bourbaki, *Topological Vector Spaces*, III §1.6][bourbaki1987] -/
theorem isCompact_closure_of_totallyBounded_quasiComplete {E : Type*} {𝕜 : Type*} [NormedField 𝕜] [AddCommGroup E]
    [Module 𝕜 E] [UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜 E] [QuasiCompleteSpace 𝕜 E] {s : Set E}
    (hs : TotallyBounded s) : IsCompact (closure s) :=
  hs.closure.isCompact_of_isComplete
    (QuasiCompleteSpace.quasiComplete (TotallyBounded.isVonNBounded 𝕜 (TotallyBounded.closure hs)) isClosed_closure)

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