Proof of the Corollary — enclosing a bounded set in a simplex

Proved

Kakutani1941.FixedPoint.enclosing_simplex

by mikedeng1 · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

convexityp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1simplex

Every bounded set $S$ in $m$ -dimensional Euclidean space lies in an $m$ -dimensional closed simplex: there are affinely independent vertices $v_0,\ldots,v_m$ such that

S\subseteq\operatorname{conv}\{v_0,\ldots,v_m\}.

This supplies the larger simplex $S'$ used in the proof of Kakutani's Corollary. The assertion also applies to the empty set.

Formalization Note The simplex is represented as the convex hull of a finite range, with affine independence imposing full dimension.

Preamble

import Mathlib

Formal statement

namespace Kakutani1941.FixedPoint

/-- Proof of the Corollary, p. 458: a bounded set fits in a closed full simplex. -/
theorem enclosing_simplex {m : ℕ} {S : Set (EuclideanSpace ℝ (Fin m))}
    (hSbounded : Bornology.IsBounded S) :
    ∃ v : Fin (m + 1) → EuclideanSpace ℝ (Fin m),
      AffineIndependent ℝ v ∧ S ⊆ convexHull ℝ (Set.range v) := by sorry

end Kakutani1941.FixedPoint

Source

Kakutani, A generalization of Brouwer's fixed point theorem, Duke Math. J. 8 (1941), p. 458, proof of the Corollary, https://doi.org/10.1215/s0012-7094-41-00838-4

Human review

Endorsed by Shuze Chen · Oct 6, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph