convexBodySum_compact — Mathlib

English

For each B, convexBodySum K B is compact.

Русский

Для каждого B множество convexBodySum K B компактно.

LaTeX

$$IsCompact (convexBodySum K B)$$

Lean4

theorem convexBodySum_compact : IsCompact (convexBodySum K B) := by
  classical
  rw [Metric.isCompact_iff_isClosed_bounded]
  refine ⟨?_, convexBodySum_isBounded K B⟩
  convert IsClosed.preimage (convexBodySumFun_continuous K) (isClosed_Icc : IsClosed (Set.Icc 0 B))
  ext
  simp [convexBodySumFun_nonneg]

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