MATHLIBANNEX / CANONICAL DECLARATION CARD

The convex hull of a compact set in a finite real coordinate space

MathlibAnnex.isCompact_convexHull_pi

theorem

Realizes the ordinary convex hull as a finite union of compact images of bounded-length convex combinations.

Statement

If is finite and is compact, then is compact. The set may be empty.

Assumptions

The coordinate space is real and has finitely many coordinates. Only compactness of is assumed; no convexity or nonemptiness of is required.

Conclusion

The ordinary convex hull itself is compact. No closure is added to the statement. In particular the conclusion includes .

The finite dimension is used to bound the number of points in a convex representation. Compactness then comes from finitely many parameter spaces, not from an unrestricted union over all possible lengths.

Proof route

Bound the length of every convex combination by the dimension plus one, then take the finite union of the corresponding compact images.

Proof steps

  1. Write . For , put

    For , is closed and , so it is compact in finite dimensions. For , it is empty and hence compact. The finite product is compact, and is continuous as a finite sum of scalar multiplications. Thus every is compact.

  2. Every lies in by the defining property of convex combinations. Conversely, the affinely independent representation of a point in the convex hull provides finitely many points in with positive weights summing to . An affinely independent family in a -dimensional space has at most points: after choosing one point, its difference vectors are linearly independent and there are at most of them. Reindexing the representation by puts the point in for some .

  3. Thus

    The right side is a finite union of compact sets and hence compact. For , the empty weight sum is , so is empty. If is empty, is empty for every ; therefore all the images are empty, and the same union proves the empty-set case.

Main citations

Lean source signature (exact)

theorem isCompact_convexHull_pi {ι : Type*} [Fintype ι]
    (s : Set (ι → ℝ)) (hs : IsCompact s) :
    IsCompact (convexHull ℝ s)
In the source Mathematical meaning
{ι : Type*} [Fintype ι] The finite coordinate set ; its real function space is .
(s : Set (ι → ℝ)) (hs : IsCompact s) The set and the assumption that is compact. No nonemptiness or convexity is required.
In the source Mathematical meaning
convexHull ℝ s The ordinary real convex hull , without adding a closure.
IsCompact (convexHull ℝ s) The conclusion that is compact, including the empty case.
Exact surrounding binder context (separate excerpt) 
noncomputable section

open Set Finset
open scoped BigOperators

namespace MathlibAnnex

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Exact content identity

Declaration: MathlibAnnex.isCompact_convexHull_pi

Accepted content SHA-256: 633d0464ffe5488ae67fed616e5f051d32b01a50d72b4cf622df995cadeb3022

Accepted source guide SHA-256: 7292b73db6cba78516738507b2391a8ffbcff037f3a60a62414b99c0bb305964

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑