isCompact_convexHull — Mathlib

English

The convex hull of a finite set is compact.

Русский

Выпуклая оболочка конечного множества компактна.

LaTeX

$$IsCompact (convexHull ℝ s)$$

Lean4

/-- Convex hull of a finite set is compact. -/
theorem isCompact_convexHull {s : Set E} (hs : s.Finite) : IsCompact (convexHull ℝ s) :=
  by
  rw [hs.convexHull_eq_image]
  apply (@isCompact_stdSimplex _ hs.fintype).image
  haveI := hs.fintype
  apply LinearMap.continuous_on_pi

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