isCompact_closedAbsConvexHull_of_totallyBounded

English

If a subset s is totally bounded, then the closedAbsConvexHull of s is compact (in the setting of a locally convex space that is quasi-complete).

Русский

Если s полностью ограничено, то замкнутая absConvexHull(s) компактна в пространстве локально выпуклом и квази-завершённом.

LaTeX

$$$IsCompact\\bigl(\\operatorname{closedAbsConvexHull}_{\\mathbb{R}}(s)\\bigr)$$$

Lean4

/-- [Bourbaki, *Topological Vector Spaces*, III §1.6][bourbaki1987] -/
theorem isCompact_closedAbsConvexHull_of_totallyBounded {E : Type*} [AddCommGroup E] [Module ℝ E] [UniformSpace E]
    [IsUniformAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [QuasiCompleteSpace ℝ E] {s : Set E}
    (ht : TotallyBounded s) : IsCompact (closedAbsConvexHull ℝ s) :=
  by
  rw [closedAbsConvexHull_eq_closure_absConvexHull]
  exact isCompact_closure_of_totallyBounded_quasiComplete (𝕜 := ℝ) (totallyBounded_absConvexHull E ht)

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