7. Every Polytope Admits a Subdivision🔗

Theorem 7.1🔗

Theorem 7.1. For every finite S \subseteq \mathbb R^k, the polytope \operatorname{conv}(S) admits a subdivision (a finite simplicial complex with underlying space \operatorname{conv}(S)).

The proof is by strong induction on |S|, with four cases.

open Set Geometry
open scoped Topology
open _root_.FamiliesOfMapsB01

namespace Submission
namespace FamiliesOfMapsB01

variable {k : ℕ}

Case 1🔗

Case 1: S affinely independent. Take the full simplex on S: the faces are all nonempty subsets of S. Affine independence passes to subsets; downward closure is clear; and the gluing condition \operatorname{conv}(\sigma) \cap \operatorname{conv}(\tau) \subseteq \operatorname{conv}(\sigma\cap\tau) holds for subsets of an affinely independent set (faces of a simplex meet along faces, by uniqueness of barycentric coordinates). The space is \operatorname{conv}(S) (the top face). The face set is finite.

/-- The full simplex on an affinely independent vertex set `S`: its faces are all
nonempty subsets of `S`. -/
noncomputable def simplexComplex
    (S : Finset (Fin k → ℝ))
    (hS : AffineIndependent ℝ ((↑) : S → (Fin k → ℝ))) :
    SimplicialComplex ℝ (Fin k → ℝ) :=
  SimplicialComplex.ofErase
    {t : Finset (Fin k → ℝ) | t ⊆ S}
    (byk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.val⊢ ∀ s ∈ {t | t ⊆ S}, AffineIndependent ℝ Subtype.val
      intro t htk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.valt:Finset (Fin k → ℝ)ht:t ∈ {t | t ⊆ S}⊢ AffineIndependent ℝ Subtype.val
      exact hS.mono (byk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.valt:Finset (Fin k → ℝ)ht:t ∈ {t | t ⊆ S}⊢ ↑t ⊆ ↑S simpa using htAll goals completed! 🐙))
    (byk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.val⊢ IsLowerSet {t | t ⊆ S}
      intro a bk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.vala:Finset (Fin k → ℝ)b:Finset (Fin k → ℝ)⊢ b ≤ a → a ∈ {t | t ⊆ S} → b ∈ {t | t ⊆ S} habk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.vala:Finset (Fin k → ℝ)b:Finset (Fin k → ℝ)hab:b ≤ a⊢ a ∈ {t | t ⊆ S} → b ∈ {t | t ⊆ S} hbk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.vala:Finset (Fin k → ℝ)b:Finset (Fin k → ℝ)hab:b ≤ ahb:a ∈ {t | t ⊆ S}⊢ b ∈ {t | t ⊆ S}
      exact hab.trans hbAll goals completed! 🐙)
    (byk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.val⊢ ∀ s ∈ {t | t ⊆ S}, ∀ t ∈ {t | t ⊆ S}, (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)
      intro s hsk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.vals:Finset (Fin k → ℝ)hs:s ∈ {t | t ⊆ S}⊢ ∀ t ∈ {t | t ⊆ S}, (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t) tk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.vals:Finset (Fin k → ℝ)hs:s ∈ {t | t ⊆ S}t:Finset (Fin k → ℝ)⊢ t ∈ {t | t ⊆ S} → (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t) htk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.vals:Finset (Fin k → ℝ)hs:s ∈ {t | t ⊆ S}t:Finset (Fin k → ℝ)ht:t ∈ {t | t ⊆ S}⊢ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)
      have := (hS.convexHull_inter (s := S) (t₁ := s) (t₂ := t) hs ht)k:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.vals:Finset (Fin k → ℝ)hs:s ∈ {t | t ⊆ S}t:Finset (Fin k → ℝ)ht:t ∈ {t | t ⊆ S}this:(convexHull ℝ) (↑s ∩ ↑t) = (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t⊢ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t ⊆ (convexHull ℝ) (↑s ∩ ↑t)
      rw [this]All goals completed! 🐙)

lemma simplexComplex_faces
    (S : Finset (Fin k → ℝ))
    (hS : AffineIndependent ℝ ((↑) : S → (Fin k → ℝ))) :
    (simplexComplex S hS).faces = {t : Finset (Fin k → ℝ) | t ⊆ S} \ {∅} := byk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.val⊢ (simplexComplex S hS).faces = {t | t ⊆ S} \ {∅}
  rflAll goals completed! 🐙

lemma simplexComplex_faces_finite
    (S : Finset (Fin k → ℝ))
    (hS : AffineIndependent ℝ ((↑) : S → (Fin k → ℝ))) :
    (simplexComplex S hS).faces.Finite := byk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.val⊢ (simplexComplex S hS).faces.Finite
  exact Set.finite_iff_bddAbove.mpr ⟨ S, fun t ht => Finset.le_iff_subset.mpr ht.1 ⟩All goals completed! 🐙

lemma simplexComplex_space
    (S : Finset (Fin k → ℝ))
    (hS : AffineIndependent ℝ ((↑) : S → (Fin k → ℝ))) :
    (simplexComplex S hS).space = convexHull ℝ (S : Set (Fin k → ℝ)) := byk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.val⊢ (simplexComplex S hS).space = (convexHull ℝ) ↑S
  ext xhk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.valx:Fin k → ℝ⊢ x ∈ (simplexComplex S hS).space ↔ x ∈ (convexHull ℝ) ↑S
  simp [simplexComplex, SimplicialComplex.space]hk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.valx:Fin k → ℝ⊢ (∃ i, (i ⊆ S ∧ ¬i = ∅) ∧ x ∈ (convexHull ℝ) ↑i) ↔ x ∈ (convexHull ℝ) ↑S;
  constructorh.mpk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.valx:Fin k → ℝ⊢ (∃ i, (i ⊆ S ∧ ¬i = ∅) ∧ x ∈ (convexHull ℝ) ↑i) → x ∈ (convexHull ℝ) ↑Sh.mprk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.valx:Fin k → ℝ⊢ x ∈ (convexHull ℝ) ↑S → ∃ i, (i ⊆ S ∧ ¬i = ∅) ∧ x ∈ (convexHull ℝ) ↑i;
  ·h.mpk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.valx:Fin k → ℝ⊢ (∃ i, (i ⊆ S ∧ ¬i = ∅) ∧ x ∈ (convexHull ℝ) ↑i) → x ∈ (convexHull ℝ) ↑S rintro ⟨ i, hi, hx ⟩h.mpk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.valx:Fin k → ℝi:Finset (Fin k → ℝ)hi:i ⊆ S ∧ ¬i = ∅hx:x ∈ (convexHull ℝ) ↑i⊢ x ∈ (convexHull ℝ) ↑S ; exact convexHull_mono ( Finset.coe_subset.mpr hi.1 ) hxAll goals completed! 🐙;
  ·h.mprk:ℕS:Finset (Fin k → ℝ)hS:AffineIndependent ℝ Subtype.valx:Fin k → ℝ⊢ x ∈ (convexHull ℝ) ↑S → ∃ i, (i ⊆ S ∧ ¬i = ∅) ∧ x ∈ (convexHull ℝ) ↑i aesopAll goals completed! 🐙

/-- If `P` is the convex hull of an affinely independent finite set, it admits a
polyhedral subdivision (namely, the full simplex on its vertices). -/
noncomputable def simplexSubdivision
    (S : Finset (Fin k → ℝ))
    (hS : AffineIndependent ℝ ((↑) : S → (Fin k → ℝ))) :
    Subdivision (convexHull ℝ (S : Set (Fin k → ℝ))) where
  complex := simplexComplex S hS
  faces_finite := simplexComplex_faces_finite S hS
  space_eq := simplexComplex_space S hS

lemma simplex_has_subdivision
    (S : Finset (Fin k → ℝ))
    (hS : AffineIndependent ℝ ((↑) : S → (Fin k → ℝ))) :
    Nonempty (Subdivision (convexHull ℝ (S : Set (Fin k → ℝ)))) :=
  ⟨simplexSubdivision S hS⟩

Case 2🔗

Case 2: some v \in S is redundant, i.e. v \in \operatorname{conv}(S \smallsetminus \{v\}). Then \operatorname{conv}(S) = \operatorname{conv}(S \smallsetminus \{v\}), and the inductive hypothesis applies to S \smallsetminus \{v\}.

/-
Removing a point that already lies in the convex hull of the remaining points does
not change the convex hull.  This lets us reduce triangulation existence for an
arbitrary finite point set to the case of an *irredundant* set (one where every point
is a genuine vertex of the polytope).
-/
lemma convexHull_erase_of_mem
    {S : Finset (Fin k → ℝ)} {v : Fin k → ℝ}
    (hmem : v ∈ convexHull ℝ ((S.erase v : Finset (Fin k → ℝ)) : Set (Fin k → ℝ))) :
    convexHull ℝ (S : Set (Fin k → ℝ))
      = convexHull ℝ ((S.erase v : Finset (Fin k → ℝ)) : Set (Fin k → ℝ)) := byk:ℕS:Finset (Fin k → ℝ)v:Fin k → ℝhmem:v ∈ (convexHull ℝ) ↑(S.erase v)⊢ (convexHull ℝ) ↑S = (convexHull ℝ) ↑(S.erase v)
  refine' le_antisymm _ _refine'_1k:ℕS:Finset (Fin k → ℝ)v:Fin k → ℝhmem:v ∈ (convexHull ℝ) ↑(S.erase v)⊢ (convexHull ℝ) ↑S ≤ (convexHull ℝ) ↑(S.erase v)refine'_2k:ℕS:Finset (Fin k → ℝ)v:Fin k → ℝhmem:v ∈ (convexHull ℝ) ↑(S.erase v)⊢ (convexHull ℝ) ↑(S.erase v) ≤ (convexHull ℝ) ↑S;
  ·refine'_1k:ℕS:Finset (Fin k → ℝ)v:Fin k → ℝhmem:v ∈ (convexHull ℝ) ↑(S.erase v)⊢ (convexHull ℝ) ↑S ≤ (convexHull ℝ) ↑(S.erase v) refine' convexHull_min _ _refine'_1.refine'_1k:ℕS:Finset (Fin k → ℝ)v:Fin k → ℝhmem:v ∈ (convexHull ℝ) ↑(S.erase v)⊢ ↑S ⊆ (convexHull ℝ) ↑(S.erase v)refine'_1.refine'_2k:ℕS:Finset (Fin k → ℝ)v:Fin k → ℝhmem:v ∈ (convexHull ℝ) ↑(S.erase v)⊢ Convex ℝ ((convexHull ℝ) ↑(S.erase v));
    ·refine'_1.refine'_1k:ℕS:Finset (Fin k → ℝ)v:Fin k → ℝhmem:v ∈ (convexHull ℝ) ↑(S.erase v)⊢ ↑S ⊆ (convexHull ℝ) ↑(S.erase v) exact fun x hx => if hxv : x = v then hxv.symm ▸ hmem else subset_convexHull ℝ _ ( byk:ℕS:Finset (Fin k → ℝ)v:Fin k → ℝhmem:v ∈ (convexHull ℝ) ↑(S.erase v)x:Fin k → ℝhx:x ∈ ↑Shxv:¬x = v⊢ x ∈ ↑(S.erase v) aesopAll goals completed! 🐙 );
    ·refine'_1.refine'_2k:ℕS:Finset (Fin k → ℝ)v:Fin k → ℝhmem:v ∈ (convexHull ℝ) ↑(S.erase v)⊢ Convex ℝ ((convexHull ℝ) ↑(S.erase v)) exact convex_convexHull ℝ _All goals completed! 🐙;
  ·refine'_2k:ℕS:Finset (Fin k → ℝ)v:Fin k → ℝhmem:v ∈ (convexHull ℝ) ↑(S.erase v)⊢ (convexHull ℝ) ↑(S.erase v) ≤ (convexHull ℝ) ↑S exact convexHull_mono ( Finset.coe_subset.mpr ( Finset.erase_subset _ _ ) )All goals completed! 🐙

Case 3🔗

Case 3: not Case 1 or 2, and some v \in S is an apex: S \smallsetminus \{v\} \ne \emptyset and v is not in the affine span of S \smallsetminus \{v\}. Let K be a subdivision of P' := \operatorname{conv}(S \smallsetminus \{v\}) (inductive hypothesis) and form the cone on K with apex v: its faces are the faces \sigma of K, the sets \{v\} \cup \sigma for \sigma a face of K, and \{v\}. We check this is a simplicial complex:

The cone construction and its verification (affine independence, downward closure, gluing via the unique apex height) are developed in the cone subdivisions chapter; here it is packaged as a subdivision:

/-- **Apex / dimension-raising reduction.** If `P` is a nonempty subdivided polytope and
`v` lies off `affineSpan ℝ P`, then the cone `convexJoin ℝ {v} P` (a one-higher-dimensional
polytope) is itself subdivided, by coning the given subdivision of `P` along the cone API
of `Submission/Cone.lean`. -/
noncomputable def coneSubdivision {P : Set (Fin k → ℝ)}
    (v : Fin k → ℝ) (hv : v ∉ affineSpan ℝ P) (hne : P.Nonempty) (K : Subdivision P) :
    Subdivision (convexJoin ℝ {v} P) where
  complex := coneComplex v K.complex (byk:ℕP:Set (Fin k → ℝ)v:Fin k → ℝhv:v ∉ affineSpan ℝ Phne:P.NonemptyK:Subdivision P⊢ v ∉ affineSpan ℝ K.complex.space rw [K.space_eq]k:ℕP:Set (Fin k → ℝ)v:Fin k → ℝhv:v ∉ affineSpan ℝ Phne:P.NonemptyK:Subdivision P⊢ v ∉ affineSpan ℝ P; exact hvAll goals completed! 🐙)
  faces_finite := coneComplex_faces_finite v K.complex _ K.faces_finite
  space_eq := byk:ℕP:Set (Fin k → ℝ)v:Fin k → ℝhv:v ∉ affineSpan ℝ Phne:P.NonemptyK:Subdivision P⊢ (coneComplex v K.complex ⋯).space = convexJoin ℝ {v} P
    rw [coneComplex_space v K.complex _ (by rw [K.space_eq]; exact hne), K.space_eq]All goals completed! 🐙

/-- The convex hull of `insert v S'` is the cone (convex join) of `v` over the convex
hull of a nonempty `S'`. -/
lemma convexHull_insert_eq_join (v : Fin k → ℝ) (S' : Finset (Fin k → ℝ))
    (hS' : S'.Nonempty) :
    convexHull ℝ ((insert v S' : Finset (Fin k → ℝ)) : Set (Fin k → ℝ))
      = convexJoin ℝ {v} (convexHull ℝ (S' : Set (Fin k → ℝ))) := byk:ℕv:Fin k → ℝS':Finset (Fin k → ℝ)hS':S'.Nonempty⊢ (convexHull ℝ) ↑(insert v S') = convexJoin ℝ {v} ((convexHull ℝ) ↑S')
  rw [Finset.coe_insert]k:ℕv:Fin k → ℝS':Finset (Fin k → ℝ)hS':S'.Nonempty⊢ (convexHull ℝ) (insert v ↑S') = convexJoin ℝ {v} ((convexHull ℝ) ↑S')
  exact convexHull_insert (Finset.coe_nonempty.mpr hS')All goals completed! 🐙

The space of the cone is the join \{(1-a)v + a\,b : a \in [0,1],\ b \in P'\}, which equals \operatorname{conv}(\{v\} \cup (S\smallsetminus\{v\})) = \operatorname{conv}(S). Finiteness is clear.

(An auxiliary separating-functional lemma sits alongside the cone reduction in the original development:)

/-- At an irredundant vertex `v` of `S` there is a linear functional strictly
separating `v` from all other vertices (`geometric_hahn_banach` on the closed convex
`convexHull (S.erase v)`).  This is the supporting functional that the slice/cone
decomposition pulls `v` along: every other vertex, hence the whole opposite face, lies
strictly below `φ v`. -/
lemma exists_separating_functional_of_vertex
    (S : Finset (Fin k → ℝ)) (v : Fin k → ℝ)
    (hirr : v ∉ convexHull ℝ ((S.erase v : Finset (Fin k → ℝ)) : Set (Fin k → ℝ))) :
    ∃ (φ : (Fin k → ℝ) →ₗ[ℝ] ℝ), ∀ w ∈ S.erase v, φ w < φ v := byk:ℕS:Finset (Fin k → ℝ)v:Fin k → ℝhirr:v ∉ (convexHull ℝ) ↑(S.erase v)⊢ ∃ φ, ∀ w ∈ S.erase v, φ w < φ v
  obtain ⟨f, u, hf, hu⟩ := geometric_hahn_banach_closed_point (convex_convexHull ℝ _)
    (((S.erase v).finite_toSet.isCompact_convexHull (𝕜 := ℝ)).isClosed) hirrk:ℕS:Finset (Fin k → ℝ)v:Fin k → ℝhirr:v ∉ (convexHull ℝ) ↑(S.erase v)f:StrongDual ℝ (Fin k → ℝ)u:ℝhf:∀ a ∈ (convexHull ℝ) ↑(S.erase v), f a < uhu:u < f v⊢ ∃ φ, ∀ w ∈ S.erase v, φ w < φ v
  refine ⟨f.toLinearMap, ?_⟩k:ℕS:Finset (Fin k → ℝ)v:Fin k → ℝhirr:v ∉ (convexHull ℝ) ↑(S.erase v)f:StrongDual ℝ (Fin k → ℝ)u:ℝhf:∀ a ∈ (convexHull ℝ) ↑(S.erase v), f a < uhu:u < f v⊢ ∀ w ∈ S.erase v, ↑f w < ↑f v
  intro w hwk:ℕS:Finset (Fin k → ℝ)v:Fin k → ℝhirr:v ∉ (convexHull ℝ) ↑(S.erase v)f:StrongDual ℝ (Fin k → ℝ)u:ℝhf:∀ a ∈ (convexHull ℝ) ↑(S.erase v), f a < uhu:u < f vw:Fin k → ℝhw:w ∈ S.erase v⊢ ↑f w < ↑f v
  have : f w < u := hf w (subset_convexHull ℝ _ hw)k:ℕS:Finset (Fin k → ℝ)v:Fin k → ℝhirr:v ∉ (convexHull ℝ) ↑(S.erase v)f:StrongDual ℝ (Fin k → ℝ)u:ℝhf:∀ a ∈ (convexHull ℝ) ↑(S.erase v), f a < uhu:u < f vw:Fin k → ℝhw:w ∈ S.erase vthis:f w < u⊢ ↑f w < ↑f v
  simpa using this.trans huAll goals completed! 🐙

Case 4🔗

Case 4: none of the above — S is affinely dependent, irredundant (no vertex in the hull of the others), and flat: every v \in S lies in the affine span of S \smallsetminus \{v\}. (The simplest example: the four corners of a square.) Here one uses the regular (lower-envelope) triangulation, which we now construct. (The regular triangulation in fact works for arbitrary finite S, making Cases 1–3 logically dispensable; we retain the induction because the earlier cases are elementary, and invoke the regular triangulation only in this residual case.)

The regular triangulation is constructed in the regular triangulation chapter; the flat case invokes it:

/-- **The genuine residual triangulation problem (flat case).** An *irredundant* finite
vertex set `S` (every point is a real vertex of the polytope) that is **not** affinely
independent and is moreover *flat*: every vertex lies in the affine span of the others
(so no vertex is an apex that the cone reduction `coneSubdivision` could strip off).  The
simplest example is the four corners of a square.  Triangulating such a polytope without
introducing Steiner points is the classical *pulling/placing* triangulation, which
requires a visible-facet / boundary-complex API that Mathlib does not provide.  This
isolated statement is the precise remaining geometric blocker for general triangulation
existence (and hence for conjunct 2 of Morrison–Walker B.0.1). -/
theorem polytope_flat_has_subdivision
    (S : Finset (Fin k → ℝ))
    (_hirr : ∀ v ∈ S,
        v ∉ convexHull ℝ ((S.erase v : Finset (Fin k → ℝ)) : Set (Fin k → ℝ)))
    (_hdep : ¬ AffineIndependent ℝ ((↑) : S → (Fin k → ℝ)))
    (_hflat : ∀ v ∈ S,
        v ∈ affineSpan ℝ ((S.erase v : Finset (Fin k → ℝ)) : Set (Fin k → ℝ))) :
    Nonempty (Subdivision (convexHull ℝ (S : Set (Fin k → ℝ)))) :=
  Submission.FamiliesOfMapsB01Regular.regular_subdivision_exists S

The strong induction assembling the four cases, and the form of the result used throughout the main text:

/-- **General triangulation existence.** Every polytope `convexHull ℝ S` (the convex
hull of a finite point set in `ℝᵏ`) admits a polyhedral subdivision.  The proof reduces
(by strong induction on `S.card`): discard redundant points via `convexHull_erase_of_mem`;
use `simplex_has_subdivision` for the affinely independent base case; strip off an *apex*
vertex `v ∉ affineSpan` of the rest via `coneSubdivision`; leaving only the irredundant,
affinely dependent, *flat* case handled by `polytope_flat_has_subdivision` — the one
genuinely missing piece (the pulling triangulation). -/
theorem polytope_has_subdivision
    (S : Finset (Fin k → ℝ)) :
    Nonempty (Subdivision (convexHull ℝ (S : Set (Fin k → ℝ)))) := byk:ℕS:Finset (Fin k → ℝ)⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
  classical
  induction hc : S.card using Nat.strong_induction_on generalizing S with
  | _ n IH =>hk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = n⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
    by_cases hai : AffineIndependent ℝ ((↑) : S → (Fin k → ℝ))posk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:AffineIndependent ℝ Subtype.val⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))negk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.val⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
    ·posk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:AffineIndependent ℝ Subtype.val⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S)) exact simplex_has_subdivision S haiAll goals completed! 🐙
    ·negk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.val⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S)) by_cases hred : ∃ v ∈ S,
          v ∈ convexHull ℝ ((S.erase v : Finset (Fin k → ℝ)) : Set (Fin k → ℝ))posk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∃ v ∈ S, v ∈ (convexHull ℝ) ↑(S.erase v)⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))negk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:¬∃ v ∈ S, v ∈ (convexHull ℝ) ↑(S.erase v)⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
      ·posk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∃ v ∈ S, v ∈ (convexHull ℝ) ↑(S.erase v)⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S)) obtain ⟨v, hvS, hvmem⟩ := hredposk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valv:Fin k → ℝhvS:v ∈ Shvmem:v ∈ (convexHull ℝ) ↑(S.erase v)⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
        have hpos : 0 < S.card := Finset.card_pos.mpr ⟨v, hvS⟩posk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valv:Fin k → ℝhvS:v ∈ Shvmem:v ∈ (convexHull ℝ) ↑(S.erase v)hpos:0 < S.card⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
        have hlt : (S.erase v).card < n := byk:ℕS:Finset (Fin k → ℝ)⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
          rw [Finset.card_erase_of_mem hvS]k:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valv:Fin k → ℝhvS:v ∈ Shvmem:v ∈ (convexHull ℝ) ↑(S.erase v)hpos:0 < S.card⊢ S.card - 1 < n; omegaAll goals completed! 🐙
        have hsub := IH (S.erase v).card (hc ▸ hlt) (S.erase v) rflposk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valv:Fin k → ℝhvS:v ∈ Shvmem:v ∈ (convexHull ℝ) ↑(S.erase v)hpos:0 < S.cardhlt:(S.erase v).card < nhsub:Nonempty (Subdivision ((convexHull ℝ) ↑(S.erase v)))⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
        rwa [convexHull_erase_of_mem hvmem]posk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valv:Fin k → ℝhvS:v ∈ Shvmem:v ∈ (convexHull ℝ) ↑(S.erase v)hpos:0 < S.cardhlt:(S.erase v).card < nhsub:Nonempty (Subdivision ((convexHull ℝ) ↑(S.erase v)))⊢ Nonempty (Subdivision ((convexHull ℝ) ↑(S.erase v)))
      ·negk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:¬∃ v ∈ S, v ∈ (convexHull ℝ) ↑(S.erase v)⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S)) `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
push_neg at hrednegk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
        by_cases hapex : ∃ v ∈ S, (S.erase v).Nonempty ∧
            v ∉ affineSpan ℝ ((S.erase v : Finset (Fin k → ℝ)) : Set (Fin k → ℝ))posk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)hapex:∃ v ∈ S, (S.erase v).Nonempty ∧ v ∉ affineSpan ℝ ↑(S.erase v)⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))negk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)hapex:¬∃ v ∈ S, (S.erase v).Nonempty ∧ v ∉ affineSpan ℝ ↑(S.erase v)⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
        ·posk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)hapex:∃ v ∈ S, (S.erase v).Nonempty ∧ v ∉ affineSpan ℝ ↑(S.erase v)⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S)) obtain ⟨v, hvS, hne, hv⟩ := hapexposk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Shne:(S.erase v).Nonemptyhv:v ∉ affineSpan ℝ ↑(S.erase v)⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
          have hpos : 0 < S.card := Finset.card_pos.mpr ⟨v, hvS⟩posk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Shne:(S.erase v).Nonemptyhv:v ∉ affineSpan ℝ ↑(S.erase v)hpos:0 < S.card⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
          have hlt : (S.erase v).card < n := byk:ℕS:Finset (Fin k → ℝ)⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
            rw [Finset.card_erase_of_mem hvS]k:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Shne:(S.erase v).Nonemptyhv:v ∉ affineSpan ℝ ↑(S.erase v)hpos:0 < S.card⊢ S.card - 1 < n; omegaAll goals completed! 🐙
          obtain ⟨K⟩ := IH (S.erase v).card (hc ▸ hlt) (S.erase v) rflposk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Shne:(S.erase v).Nonemptyhv:v ∉ affineSpan ℝ ↑(S.erase v)hpos:0 < S.cardhlt:(S.erase v).card < nK:Subdivision ((convexHull ℝ) ↑(S.erase v))⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
          have hPne : (convexHull ℝ ((S.erase v : Finset (Fin k → ℝ)) : Set (Fin k → ℝ))).Nonempty :=
            (Finset.coe_nonempty.mpr hne).convexHullposk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Shne:(S.erase v).Nonemptyhv:v ∉ affineSpan ℝ ↑(S.erase v)hpos:0 < S.cardhlt:(S.erase v).card < nK:Subdivision ((convexHull ℝ) ↑(S.erase v))hPne:((convexHull ℝ) ↑(S.erase v)).Nonempty⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
          have hv' : v ∉ affineSpan ℝ
              (convexHull ℝ ((S.erase v : Finset (Fin k → ℝ)) : Set (Fin k → ℝ))) := byk:ℕS:Finset (Fin k → ℝ)⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
            rwa [affineSpan_convexHull]k:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Shne:(S.erase v).Nonemptyhv:v ∉ affineSpan ℝ ↑(S.erase v)hpos:0 < S.cardhlt:(S.erase v).card < nK:Subdivision ((convexHull ℝ) ↑(S.erase v))hPne:((convexHull ℝ) ↑(S.erase v)).Nonempty⊢ v ∉ affineSpan ℝ ↑(S.erase v)
          refine ⟨?_⟩posk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Shne:(S.erase v).Nonemptyhv:v ∉ affineSpan ℝ ↑(S.erase v)hpos:0 < S.cardhlt:(S.erase v).card < nK:Subdivision ((convexHull ℝ) ↑(S.erase v))hPne:((convexHull ℝ) ↑(S.erase v)).Nonemptyhv':v ∉ affineSpan ℝ ((convexHull ℝ) ↑(S.erase v))⊢ Subdivision ((convexHull ℝ) ↑S)
          rw [show convexHull ℝ ((S : Finset (Fin k → ℝ)) : Set (Fin k → ℝ))
                = convexJoin ℝ {v}
                    (convexHull ℝ ((S.erase v : Finset (Fin k → ℝ)) : Set (Fin k → ℝ))) by
            rw [← convexHull_insert_eq_join v (S.erase v) hne, Finset.insert_erase hvS]]posk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Shne:(S.erase v).Nonemptyhv:v ∉ affineSpan ℝ ↑(S.erase v)hpos:0 < S.cardhlt:(S.erase v).card < nK:Subdivision ((convexHull ℝ) ↑(S.erase v))hPne:((convexHull ℝ) ↑(S.erase v)).Nonemptyhv':v ∉ affineSpan ℝ ((convexHull ℝ) ↑(S.erase v))⊢ Subdivision (convexJoin ℝ {v} ((convexHull ℝ) ↑(S.erase v)))
          exact coneSubdivision v hv' hPne KAll goals completed! 🐙
        ·negk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)hapex:¬∃ v ∈ S, (S.erase v).Nonempty ∧ v ∉ affineSpan ℝ ↑(S.erase v)⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S)) `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
push_neg at hapexnegk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)hapex:∀ v ∈ S, (S.erase v).Nonempty → v ∈ affineSpan ℝ ↑(S.erase v)⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
          refine polytope_flat_has_subdivision S hred hai ?_negk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)hapex:∀ v ∈ S, (S.erase v).Nonempty → v ∈ affineSpan ℝ ↑(S.erase v)⊢ ∀ v ∈ S, v ∈ affineSpan ℝ ↑(S.erase v)
          intro v hvSnegk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)hapex:∀ v ∈ S, (S.erase v).Nonempty → v ∈ affineSpan ℝ ↑(S.erase v)v:Fin k → ℝhvS:v ∈ S⊢ v ∈ affineSpan ℝ ↑(S.erase v)
          by_cases hne : (S.erase v).Nonemptyposk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)hapex:∀ v ∈ S, (S.erase v).Nonempty → v ∈ affineSpan ℝ ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Shne:(S.erase v).Nonempty⊢ v ∈ affineSpan ℝ ↑(S.erase v)negk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)hapex:∀ v ∈ S, (S.erase v).Nonempty → v ∈ affineSpan ℝ ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Shne:¬(S.erase v).Nonempty⊢ v ∈ affineSpan ℝ ↑(S.erase v)
          ·posk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)hapex:∀ v ∈ S, (S.erase v).Nonempty → v ∈ affineSpan ℝ ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Shne:(S.erase v).Nonempty⊢ v ∈ affineSpan ℝ ↑(S.erase v) exact hapex v hvS hneAll goals completed! 🐙
          ·negk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)hapex:∀ v ∈ S, (S.erase v).Nonempty → v ∈ affineSpan ℝ ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Shne:¬(S.erase v).Nonempty⊢ v ∈ affineSpan ℝ ↑(S.erase v) exfalsonegk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)hapex:∀ v ∈ S, (S.erase v).Nonempty → v ∈ affineSpan ℝ ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Shne:¬(S.erase v).Nonempty⊢ False
            rw [Finset.not_nonempty_iff_eq_empty, Finset.erase_eq_empty_iff] at hnenegk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)hapex:∀ v ∈ S, (S.erase v).Nonempty → v ∈ affineSpan ℝ ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Shne:S = ∅ ∨ S = {v}⊢ False
            rcases hne with h | hneg.inlk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)hapex:∀ v ∈ S, (S.erase v).Nonempty → v ∈ affineSpan ℝ ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Sh:S = ∅⊢ Falseneg.inrk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)hapex:∀ v ∈ S, (S.erase v).Nonempty → v ∈ affineSpan ℝ ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Sh:S = {v}⊢ False
            ·neg.inlk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)hapex:∀ v ∈ S, (S.erase v).Nonempty → v ∈ affineSpan ℝ ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Sh:S = ∅⊢ False subst hneg.inlk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))v:Fin k → ℝhc:∅.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ ∅, v ∉ (convexHull ℝ) ↑(∅.erase v)hapex:∀ v ∈ ∅, (∅.erase v).Nonempty → v ∈ affineSpan ℝ ↑(∅.erase v)hvS:v ∈ ∅⊢ False; simp at hvSAll goals completed! 🐙
            ·neg.inrk:ℕn:ℕIH:∀ m < n, ∀ (S : Finset (Fin k → ℝ)), S.card = m → Nonempty (Subdivision ((convexHull ℝ) ↑S))S:Finset (Fin k → ℝ)hc:S.card = nhai:¬AffineIndependent ℝ Subtype.valhred:∀ v ∈ S, v ∉ (convexHull ℝ) ↑(S.erase v)hapex:∀ v ∈ S, (S.erase v).Nonempty → v ∈ affineSpan ℝ ↑(S.erase v)v:Fin k → ℝhvS:v ∈ Sh:S = {v}⊢ False exact hai (h ▸ affineIndependent_of_subsingleton ℝ _)All goals completed! 🐙

/-- Equivalently, every `IsPolyhedron P` admits a subdivision. -/
theorem isPolyhedron_has_subdivision
    {P : Set (Fin k → ℝ)} (hP : IsPolyhedron P) :
    Nonempty (Subdivision P) := byk:ℕP:Set (Fin k → ℝ)hP:IsPolyhedron P⊢ Nonempty (Subdivision P)
  obtain ⟨S, rfl⟩ := hPk:ℕS:Finset (Fin k → ℝ)⊢ Nonempty (Subdivision ((convexHull ℝ) ↑S))
  exact polytope_has_subdivision SAll goals completed! 🐙

end FamiliesOfMapsB01
end Submission