Adapting Families of Maps to Open Covers

Auxiliary InfrastructureπŸ”—

The formalization contains five further files: infrastructure developed en route that the finished proof does not use. They are reproduced here so that the site carries the complete development.

Exposed faces of a polytopeπŸ”—

From Facets.lean: for a finite vertex set S and a linear functional \varphi, the exposed face \{x \in \operatorname{conv}(S) : \varphi x = M\} (where M is the maximum of \varphi over the polytope) equals the convex hull of the maximizing vertices; two exposed faces meet in the exposed face of the summed functional. This was built toward a pulling triangulation, before the regular triangulation superseded it.

open Set open scoped Topology BigOperators namespace Submission namespace FamiliesOfMapsB01Facets variable {k : β„•} /- A linear functional attains a maximum on the convex hull of a finite nonempty set, and that maximum is attained at one of the generating points. -/ lemma exists_max_vertex (S : Finset (Fin k β†’ ℝ)) (hS : S.Nonempty) (Ο† : (Fin k β†’ ℝ) β†’β‚—[ℝ] ℝ) : βˆƒ v ∈ S, βˆ€ x ∈ convexHull ℝ (S : Set (Fin k β†’ ℝ)), Ο† x ≀ Ο† v := k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„βŠ’ βˆƒ v ∈ S, βˆ€ x ∈ (convexHull ℝ) ↑S, Ο† x ≀ Ο† v -- By definition of convex hull, any point in the convex hull of S can be written as a convex combination of points in S. have h_convex_comb : βˆ€ x ∈ convexHull ℝ (S : Set ((Fin k) β†’ ℝ)), βˆƒ (w : (Fin k β†’ ℝ) β†’ ℝ), (βˆ€ v ∈ S, 0 ≀ w v) ∧ (βˆ‘ v ∈ S, w v = 1) ∧ x = βˆ‘ v ∈ S, w v β€’ v := k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„βŠ’ βˆƒ v ∈ S, βˆ€ x ∈ (convexHull ℝ) ↑S, Ο† x ≀ Ο† v intro x k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝx:Fin k β†’ ℝhx:x ∈ (convexHull ℝ) ↑S⊒ βˆƒ w, (βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ v k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝx:Fin k β†’ ℝhx:x ∈ {x | βˆƒ ΞΉ t w z, (βˆ€ i ∈ t, 0 ≀ w i) ∧ βˆ‘ i ∈ t, w i = 1 ∧ (βˆ€ i ∈ t, z i ∈ ↑S) ∧ t.centerMass w z = x}⊒ βˆƒ w, (βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ v k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝx:Fin k β†’ ℝw:Typehw:βˆƒ t w_1 z, (βˆ€ i ∈ t, 0 ≀ w_1 i) ∧ βˆ‘ i ∈ t, w_1 i = 1 ∧ (βˆ€ i ∈ t, z i ∈ ↑S) ∧ t.centerMass w_1 z = x⊒ βˆƒ w, (βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ v; k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝw✝:Typet:Finset w✝w:w✝ β†’ ℝz:w✝ β†’ Fin k β†’ ℝhw₁:βˆ€ i ∈ t, 0 ≀ w ihwβ‚‚:βˆ‘ i ∈ t, w i = 1hw₃:βˆ€ i ∈ t, z i ∈ ↑S⊒ βˆƒ w_1, (βˆ€ v ∈ S, 0 ≀ w_1 v) ∧ βˆ‘ v ∈ S, w_1 v = 1 ∧ t.centerMass w z = βˆ‘ v ∈ S, w_1 v β€’ v; k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝw✝:Typet:Finset w✝w:w✝ β†’ ℝz:w✝ β†’ Fin k β†’ ℝhw₁:βˆ€ i ∈ t, 0 ≀ w ihwβ‚‚:βˆ‘ i ∈ t, w i = 1hw₃:βˆ€ i ∈ t, z i ∈ ↑S⊒ (βˆ€ v ∈ S, 0 ≀ (fun v => βˆ‘ i ∈ t with z i = v, w i) v) ∧ βˆ‘ v ∈ S, (fun v => βˆ‘ i ∈ t with z i = v, w i) v = 1 ∧ t.centerMass w z = βˆ‘ v ∈ S, (fun v => βˆ‘ i ∈ t with z i = v, w i) v β€’ v; k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝw✝:Typet:Finset w✝w:w✝ β†’ ℝz:w✝ β†’ Fin k β†’ ℝhw₁:βˆ€ i ∈ t, 0 ≀ w ihwβ‚‚:βˆ‘ i ∈ t, w i = 1hw₃:βˆ€ i ∈ t, z i ∈ S⊒ (βˆ€ v ∈ S, 0 ≀ βˆ‘ i ∈ t with z i = v, w i) ∧ βˆ‘ x ∈ S, βˆ‘ i ∈ t with z i = x, w i = 1 ∧ βˆ‘ i ∈ t, w i β€’ z i = βˆ‘ x ∈ S, (βˆ‘ i ∈ t with z i = x, w i) β€’ x ; k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝw✝:Typet:Finset w✝w:w✝ β†’ ℝz:w✝ β†’ Fin k β†’ ℝhw₁:βˆ€ i ∈ t, 0 ≀ w ihwβ‚‚:βˆ‘ i ∈ t, w i = 1hw₃:βˆ€ i ∈ t, z i ∈ S⊒ βˆ‘ x ∈ S, βˆ‘ i ∈ t with z i = x, w i = 1k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝw✝:Typet:Finset w✝w:w✝ β†’ ℝz:w✝ β†’ Fin k β†’ ℝhw₁:βˆ€ i ∈ t, 0 ≀ w ihwβ‚‚:βˆ‘ i ∈ t, w i = 1hw₃:βˆ€ i ∈ t, z i ∈ S⊒ βˆ‘ i ∈ t, w i β€’ z i = βˆ‘ x ∈ S, (βˆ‘ i ∈ t with z i = x, w i) β€’ x; k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝw✝:Typet:Finset w✝w:w✝ β†’ ℝz:w✝ β†’ Fin k β†’ ℝhw₁:βˆ€ i ∈ t, 0 ≀ w ihwβ‚‚:βˆ‘ i ∈ t, w i = 1hw₃:βˆ€ i ∈ t, z i ∈ S⊒ βˆ‘ x ∈ S, βˆ‘ i ∈ t with z i = x, w i = 1 k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝw✝:Typet:Finset w✝w:w✝ β†’ ℝz:w✝ β†’ Fin k β†’ ℝhw₁:βˆ€ i ∈ t, 0 ≀ w ihwβ‚‚:βˆ‘ i ∈ t, w i = 1hw₃:βˆ€ i ∈ t, z i ∈ S⊒ βˆ€ i ∈ t, z i ∈ S ; All goals completed! πŸ™; k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝw✝:Typet:Finset w✝w:w✝ β†’ ℝz:w✝ β†’ Fin k β†’ ℝhw₁:βˆ€ i ∈ t, 0 ≀ w ihwβ‚‚:βˆ‘ i ∈ t, w i = 1hw₃:βˆ€ i ∈ t, z i ∈ S⊒ βˆ‘ i ∈ t, w i β€’ z i = βˆ‘ x ∈ S, (βˆ‘ i ∈ t with z i = x, w i) β€’ x k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝw✝:Typet:Finset w✝w:w✝ β†’ ℝz:w✝ β†’ Fin k β†’ ℝhw₁:βˆ€ i ∈ t, 0 ≀ w ihwβ‚‚:βˆ‘ i ∈ t, w i = 1hw₃:βˆ€ i ∈ t, z i ∈ S⊒ βˆ‘ i ∈ t, w i β€’ z i = βˆ‘ x ∈ S, βˆ‘ x_1 ∈ t, if z x_1 = x then w x_1 β€’ x else 0; k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝw✝:Typet:Finset w✝w:w✝ β†’ ℝz:w✝ β†’ Fin k β†’ ℝhw₁:βˆ€ i ∈ t, 0 ≀ w ihwβ‚‚:βˆ‘ i ∈ t, w i = 1hw₃:βˆ€ i ∈ t, z i ∈ S⊒ βˆ€ x ∈ t, w x β€’ z x = βˆ‘ x_1 ∈ S, if z x = x_1 then w x β€’ x_1 else 0 ; All goals completed! πŸ™; k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝh_convex_comb:βˆ€ x ∈ (convexHull ℝ) ↑S, βˆƒ w, (βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vv:Fin k β†’ ℝhv:v ∈ S ∧ βˆ€ x' ∈ S, Ο† x' ≀ Ο† v⊒ βˆƒ v ∈ S, βˆ€ x ∈ (convexHull ℝ) ↑S, Ο† x ≀ Ο† v; k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝh_convex_comb:βˆ€ x ∈ (convexHull ℝ) ↑S, βˆƒ w, (βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vv:Fin k β†’ ℝhv:v ∈ S ∧ βˆ€ x' ∈ S, Ο† x' ≀ Ο† vx:Fin k β†’ ℝhx:x ∈ (convexHull ℝ) ↑S⊒ Ο† x ≀ Ο† v ; k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝh_convex_comb:βˆ€ x ∈ (convexHull ℝ) ↑S, βˆƒ w, (βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vv:Fin k β†’ ℝhv:v ∈ S ∧ βˆ€ x' ∈ S, Ο† x' ≀ Ο† vw:(Fin k β†’ ℝ) β†’ ℝhw₁:βˆ€ v ∈ S, 0 ≀ w vhwβ‚‚:βˆ‘ v ∈ S, w v = 1hx:βˆ‘ v ∈ S, w v β€’ v ∈ (convexHull ℝ) ↑S⊒ Ο† (βˆ‘ v ∈ S, w v β€’ v) ≀ Ο† v ; k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝh_convex_comb:βˆ€ x ∈ (convexHull ℝ) ↑S, βˆƒ w, (βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vv:Fin k β†’ ℝhv:v ∈ S ∧ βˆ€ x' ∈ S, Ο† x' ≀ Ο† vw:(Fin k β†’ ℝ) β†’ ℝhw₁:βˆ€ v ∈ S, 0 ≀ w vhwβ‚‚:βˆ‘ v ∈ S, w v = 1hx:βˆ‘ v ∈ S, w v β€’ v ∈ (convexHull ℝ) ↑S⊒ βˆ‘ x ∈ S, w x * Ο† x ≀ Ο† v; exact le_trans ( Finset.sum_le_sum fun x hx => mul_le_mul_of_nonneg_left ( hv.2 x hx ) ( hw₁ x hx ) ) ( k:β„•S:Finset (Fin k β†’ ℝ)hS:S.NonemptyΟ†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝh_convex_comb:βˆ€ x ∈ (convexHull ℝ) ↑S, βˆƒ w, (βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vv:Fin k β†’ ℝhv:v ∈ S ∧ βˆ€ x' ∈ S, Ο† x' ≀ Ο† vw:(Fin k β†’ ℝ) β†’ ℝhw₁:βˆ€ v ∈ S, 0 ≀ w vhwβ‚‚:βˆ‘ v ∈ S, w v = 1hx:βˆ‘ v ∈ S, w v β€’ v ∈ (convexHull ℝ) ↑S⊒ βˆ‘ i ∈ S, w i * Ο† v ≀ Ο† v All goals completed! πŸ™ ) /- The maximum value of a linear functional over the convex hull of `S` equals its maximum over the finite generating set `S`. -/ lemma sSup_image_convexHull (S : Finset (Fin k β†’ ℝ)) (Ο† : (Fin k β†’ ℝ) β†’β‚—[ℝ] ℝ) (M : ℝ) (hM : βˆ€ v ∈ S, Ο† v ≀ M) : βˆ€ x ∈ convexHull ℝ (S : Set (Fin k β†’ ℝ)), Ο† x ≀ M := k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ M⊒ βˆ€ x ∈ (convexHull ℝ) ↑S, Ο† x ≀ M intro x k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ (convexHull ℝ) ↑S⊒ Ο† x ≀ M; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | βˆƒ ΞΉ t w z, (βˆ€ i ∈ t, 0 ≀ w i) ∧ βˆ‘ i ∈ t, w i = 1 ∧ (βˆ€ i ∈ t, z i ∈ ↑S) ∧ t.centerMass w z = x}⊒ Ο† x ≀ M; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typet:Finset ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhwβ‚€:βˆ€ i ∈ t, 0 ≀ w ihw₁:βˆ‘ i ∈ t, w i = 1hwβ‚‚:βˆ€ i ∈ t, z i ∈ ↑S⊒ Ο† (t.centerMass w z) ≀ M ; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typet:Finset ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhwβ‚€:βˆ€ i ∈ t, 0 ≀ w ihw₁:βˆ‘ i ∈ t, w i = 1hwβ‚‚:βˆ€ i ∈ t, z i ∈ S⊒ βˆ‘ x ∈ t, w x * Ο† (z x) ≀ M; exact le_trans ( Finset.sum_le_sum fun i hi => mul_le_mul_of_nonneg_left ( hM _ ( hwβ‚‚ i hi ) ) ( hwβ‚€ i hi ) ) ( k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typet:Finset ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhwβ‚€:βˆ€ i ∈ t, 0 ≀ w ihw₁:βˆ‘ i ∈ t, w i = 1hwβ‚‚:βˆ€ i ∈ t, z i ∈ S⊒ βˆ‘ i ∈ t, w i * M ≀ M All goals completed! πŸ™ ) /- **Exposed face = convex hull of maximizing vertices.** If `M` is the maximum of the linear functional `Ο†` over the polytope `convexHull S`, then the exposed face it cuts out is exactly the convex hull of the vertices of `S` achieving `Ο† v = M`. This gives every facet an explicit finite vertex description (a sub-`Finset` of `S`), which is what the pulling-triangulation cone step needs. -/ theorem exposedFace_eq_convexHull_maximizers (S : Finset (Fin k β†’ ℝ)) (Ο† : (Fin k β†’ ℝ) β†’β‚—[ℝ] ℝ) (M : ℝ) (hM : βˆ€ v ∈ S, Ο† v ≀ M) : {x ∈ convexHull ℝ (S : Set (Fin k β†’ ℝ)) | Ο† x = M} = convexHull ℝ ((S.filter (fun v => Ο† v = M) : Finset (Fin k β†’ ℝ)) : Set (Fin k β†’ ℝ)) := k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ M⊒ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} = (convexHull ℝ) ↑({v ∈ S | Ο† v = M}) k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ β„βŠ’ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} ↔ x ∈ (convexHull ℝ) ↑({v ∈ S | Ο† v = M}); k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ β„βŠ’ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} β†’ x ∈ (convexHull ℝ) ↑({v ∈ S | Ο† v = M})k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ β„βŠ’ x ∈ (convexHull ℝ) ↑({v ∈ S | Ο† v = M}) β†’ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ β„βŠ’ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} β†’ x ∈ (convexHull ℝ) ↑({v ∈ S | Ο† v = M})k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ β„βŠ’ x ∈ (convexHull ℝ) ↑({v ∈ S | Ο† v = M}) β†’ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ (convexHull ℝ) ↑({v ∈ S | Ο† v = M})⊒ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}⊒ x ∈ (convexHull ℝ) ↑({v ∈ S | Ο† v = M}) -- By definition of convex hull, we can write x as a convex combination of points in S. obtain ⟨w, hw⟩ : βˆƒ w : (Fin k β†’ ℝ) β†’ ℝ, (βˆ€ v ∈ S, 0 ≀ w v) ∧ (βˆ‘ v ∈ S, w v = 1) ∧ x = βˆ‘ v ∈ S, w v β€’ v := k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}⊒ βˆƒ w, (βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ v k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}this:x ∈ (convexHull ℝ) ↑S⊒ βˆƒ w, (βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ v; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}this:βˆƒ ΞΉ x_1 w z, (βˆ€ (i : ΞΉ), 0 ≀ w i) ∧ βˆ‘ i, w i = 1 ∧ (βˆ€ (i : ΞΉ), z i ∈ ↑S) ∧ βˆ‘ i, w i β€’ z i = x⊒ βˆƒ w, (βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ v; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typew✝:Fintype ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhw₁:βˆ€ (i : ΞΉ), 0 ≀ w ihwβ‚‚:βˆ‘ i, w i = 1hw₃:βˆ€ (i : ΞΉ), z i ∈ ↑Shx:βˆ‘ i, w i β€’ z i ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}⊒ βˆƒ w_1, (βˆ€ v ∈ S, 0 ≀ w_1 v) ∧ βˆ‘ v ∈ S, w_1 v = 1 ∧ βˆ‘ i, w i β€’ z i = βˆ‘ v ∈ S, w_1 v β€’ v; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typew✝:Fintype ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhw₁:βˆ€ (i : ΞΉ), 0 ≀ w ihwβ‚‚:βˆ‘ i, w i = 1hw₃:βˆ€ (i : ΞΉ), z i ∈ ↑Shx:βˆ‘ i, w i β€’ z i ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}⊒ (βˆ€ v ∈ S, 0 ≀ (fun v => βˆ‘ i with z i = v, w i) v) ∧ βˆ‘ v ∈ S, (fun v => βˆ‘ i with z i = v, w i) v = 1 ∧ βˆ‘ i, w i β€’ z i = βˆ‘ v ∈ S, (fun v => βˆ‘ i with z i = v, w i) v β€’ v; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typew✝:Fintype ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhw₁:βˆ€ (i : ΞΉ), 0 ≀ w ihwβ‚‚:βˆ‘ i, w i = 1hw₃:βˆ€ (i : ΞΉ), z i ∈ Shx:βˆ‘ i, w i β€’ z i ∈ (convexHull ℝ) ↑S ∧ βˆ‘ x, w x * Ο† (z x) = M⊒ (βˆ€ v ∈ S, 0 ≀ βˆ‘ a, if z a = v then w a else 0) ∧ (βˆ‘ x ∈ S, βˆ‘ a, if z a = x then w a else 0) = 1 ∧ βˆ‘ i, w i β€’ z i = βˆ‘ x ∈ S, (βˆ‘ a, if z a = x then w a else 0) β€’ x ; refine' ⟨ fun v hv => Finset.sum_nonneg fun i _ => k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typew✝:Fintype ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhw₁:βˆ€ (i : ΞΉ), 0 ≀ w ihwβ‚‚:βˆ‘ i, w i = 1hw₃:βˆ€ (i : ΞΉ), z i ∈ Shx:βˆ‘ i, w i β€’ z i ∈ (convexHull ℝ) ↑S ∧ βˆ‘ x, w x * Ο† (z x) = Mv:Fin k β†’ ℝhv:v ∈ Si:ΞΉx✝:i ∈ Finset.univ⊒ 0 ≀ if z i = v then w i else 0 k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typew✝:Fintype ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhw₁:βˆ€ (i : ΞΉ), 0 ≀ w ihwβ‚‚:βˆ‘ i, w i = 1hw₃:βˆ€ (i : ΞΉ), z i ∈ Shx:βˆ‘ i, w i β€’ z i ∈ (convexHull ℝ) ↑S ∧ βˆ‘ x, w x * Ο† (z x) = Mv:Fin k β†’ ℝhv:v ∈ Si:ΞΉx✝:i ∈ Finset.univh✝:z i = v⊒ 0 ≀ w ik:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typew✝:Fintype ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhw₁:βˆ€ (i : ΞΉ), 0 ≀ w ihwβ‚‚:βˆ‘ i, w i = 1hw₃:βˆ€ (i : ΞΉ), z i ∈ Shx:βˆ‘ i, w i β€’ z i ∈ (convexHull ℝ) ↑S ∧ βˆ‘ x, w x * Ο† (z x) = Mv:Fin k β†’ ℝhv:v ∈ Si:ΞΉx✝:i ∈ Finset.univh✝:Β¬z i = v⊒ 0 ≀ 0 k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typew✝:Fintype ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhw₁:βˆ€ (i : ΞΉ), 0 ≀ w ihwβ‚‚:βˆ‘ i, w i = 1hw₃:βˆ€ (i : ΞΉ), z i ∈ Shx:βˆ‘ i, w i β€’ z i ∈ (convexHull ℝ) ↑S ∧ βˆ‘ x, w x * Ο† (z x) = Mv:Fin k β†’ ℝhv:v ∈ Si:ΞΉx✝:i ∈ Finset.univh✝:z i = v⊒ 0 ≀ w ik:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typew✝:Fintype ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhw₁:βˆ€ (i : ΞΉ), 0 ≀ w ihwβ‚‚:βˆ‘ i, w i = 1hw₃:βˆ€ (i : ΞΉ), z i ∈ Shx:βˆ‘ i, w i β€’ z i ∈ (convexHull ℝ) ↑S ∧ βˆ‘ x, w x * Ο† (z x) = Mv:Fin k β†’ ℝhv:v ∈ Si:ΞΉx✝:i ∈ Finset.univh✝:Β¬z i = v⊒ 0 ≀ 0 All goals completed! πŸ™, _, _ ⟩; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typew✝:Fintype ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhw₁:βˆ€ (i : ΞΉ), 0 ≀ w ihwβ‚‚:βˆ‘ i, w i = 1hw₃:βˆ€ (i : ΞΉ), z i ∈ Shx:βˆ‘ i, w i β€’ z i ∈ (convexHull ℝ) ↑S ∧ βˆ‘ x, w x * Ο† (z x) = M⊒ (βˆ‘ x ∈ S, βˆ‘ a, if z a = x then w a else 0) = 1 k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typew✝:Fintype ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhw₁:βˆ€ (i : ΞΉ), 0 ≀ w ihwβ‚‚:βˆ‘ i, w i = 1hw₃:βˆ€ (i : ΞΉ), z i ∈ Shx:βˆ‘ i, w i β€’ z i ∈ (convexHull ℝ) ↑S ∧ βˆ‘ x, w x * Ο† (z x) = M⊒ (βˆ‘ y, βˆ‘ x ∈ S, if z y = x then w y else 0) = βˆ‘ i, w i ; All goals completed! πŸ™; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typew✝:Fintype ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhw₁:βˆ€ (i : ΞΉ), 0 ≀ w ihwβ‚‚:βˆ‘ i, w i = 1hw₃:βˆ€ (i : ΞΉ), z i ∈ Shx:βˆ‘ i, w i β€’ z i ∈ (convexHull ℝ) ↑S ∧ βˆ‘ x, w x * Ο† (z x) = M⊒ βˆ‘ i, w i β€’ z i = βˆ‘ x ∈ S, (βˆ‘ a, if z a = x then w a else 0) β€’ x k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typew✝:Fintype ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhw₁:βˆ€ (i : ΞΉ), 0 ≀ w ihwβ‚‚:βˆ‘ i, w i = 1hw₃:βˆ€ (i : ΞΉ), z i ∈ Shx:βˆ‘ i, w i β€’ z i ∈ (convexHull ℝ) ↑S ∧ βˆ‘ x, w x * Ο† (z x) = M⊒ βˆ‘ i, w i β€’ z i = βˆ‘ x, if z x ∈ S then w x β€’ z x else 0; exact Finset.sum_congr rfl fun i hi => k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typew✝:Fintype ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhw₁:βˆ€ (i : ΞΉ), 0 ≀ w ihwβ‚‚:βˆ‘ i, w i = 1hw₃:βˆ€ (i : ΞΉ), z i ∈ Shx:βˆ‘ i, w i β€’ z i ∈ (convexHull ℝ) ↑S ∧ βˆ‘ x, w x * Ο† (z x) = Mi:ΞΉhi:i ∈ Finset.univ⊒ w i β€’ z i = if z i ∈ S then w i β€’ z i else 0 All goals completed! πŸ™; -- Since $\phi(x) = M$, we have $\sum_{v \in S} w(v) \phi(v) = M$. have h_sum : βˆ‘ v ∈ S, w v * Ο† v = M := k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ M⊒ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} = (convexHull ℝ) ↑({v ∈ S | Ο† v = M}) All goals completed! πŸ™; -- Since $\phi(v) \leq M$ for all $v \in S$, and $\sum_{v \in S} w(v) \phi(v) = M$, it follows that $w(v) = 0$ for all $v \in S$ such that $\phi(v) < M$. have h_zero : βˆ€ v ∈ S, Ο† v < M β†’ w v = 0 := k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ M⊒ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} = (convexHull ℝ) ↑({v ∈ S | Ο† v = M}) intro v k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}w:(Fin k β†’ ℝ) β†’ ℝhw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mv:Fin k β†’ ℝhv:v ∈ S⊒ Ο† v < M β†’ w v = 0 k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}w:(Fin k β†’ ℝ) β†’ ℝhw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mv:Fin k β†’ ℝhv:v ∈ Shv':Ο† v < M⊒ w v = 0; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}w:(Fin k β†’ ℝ) β†’ ℝhw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vv:Fin k β†’ ℝhv:v ∈ Shv':Ο† v < Mh_sum:w v β‰  0⊒ βˆ‘ v ∈ S, w v * Ο† v β‰  M; have h_sum_lt : βˆ‘ v ∈ S, w v * Ο† v < βˆ‘ v ∈ S, w v * M := k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ M⊒ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} = (convexHull ℝ) ↑({v ∈ S | Ο† v = M}) All goals completed! πŸ™; All goals completed! πŸ™; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}w:(Fin k β†’ ℝ) β†’ ℝhw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ x ∈ {x | βˆƒ ΞΉ t w z, (βˆ€ i ∈ t, 0 ≀ w i) ∧ βˆ‘ i ∈ t, w i = 1 ∧ (βˆ€ i ∈ t, z i ∈ ↑({v ∈ S | Ο† v = M})) ∧ t.centerMass w z = x}; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}w:(Fin k β†’ ℝ) β†’ ℝhw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ βˆ€ i ∈ {v ∈ S | Ο† v = M}, 0 ≀ (fun v => w v) ik:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}w:(Fin k β†’ ℝ) β†’ ℝhw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ βˆ‘ i ∈ S with Ο† i = M, (fun v => w v) i = 1k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}w:(Fin k β†’ ℝ) β†’ ℝhw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ βˆ€ i ∈ {v ∈ S | Ο† v = M}, (fun v => v) i ∈ ↑({v ∈ S | Ο† v = M})k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}w:(Fin k β†’ ℝ) β†’ ℝhw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ ({v ∈ S | Ο† v = M}.centerMass (fun v => w v) fun v => v) = x k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}w:(Fin k β†’ ℝ) β†’ ℝhw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ βˆ€ i ∈ {v ∈ S | Ο† v = M}, 0 ≀ (fun v => w v) ik:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}w:(Fin k β†’ ℝ) β†’ ℝhw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ βˆ‘ i ∈ S with Ο† i = M, (fun v => w v) i = 1k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}w:(Fin k β†’ ℝ) β†’ ℝhw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ βˆ€ i ∈ {v ∈ S | Ο† v = M}, (fun v => v) i ∈ ↑({v ∈ S | Ο† v = M})k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}w:(Fin k β†’ ℝ) β†’ ℝhw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ ({v ∈ S | Ο† v = M}.centerMass (fun v => w v) fun v => v) = x k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝw:(Fin k β†’ ℝ) β†’ ℝhx:βˆ‘ v ∈ S, w v β€’ v ∈ (convexHull ℝ) ↑Shw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ (βˆ‘ x ∈ S with Ο† x = M, w x)⁻¹ β€’ βˆ‘ x ∈ S with Ο† x = M, w x β€’ x = βˆ‘ v ∈ S, w v β€’ v; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝw:(Fin k β†’ ℝ) β†’ ℝhx:βˆ‘ v ∈ S, w v β€’ v ∈ (convexHull ℝ) ↑Shw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ βˆ‘ x ∈ S with Ο† x = M, w x = 1 k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝw:(Fin k β†’ ℝ) β†’ ℝhx:βˆ‘ v ∈ S, w v β€’ v ∈ (convexHull ℝ) ↑Shw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ βˆ€ x ∈ S, w x β‰  0 β†’ Ο† x = M; All goals completed! πŸ™; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝw:(Fin k β†’ ℝ) β†’ ℝhx:βˆ‘ v ∈ S, w v β€’ v ∈ (convexHull ℝ) ↑Shw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ (βˆ‘ x ∈ S with Ο† x = M, w x)⁻¹ β€’ βˆ‘ x ∈ S with Ο† x = M, w x β€’ x = βˆ‘ v ∈ S, w v β€’ v k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝw:(Fin k β†’ ℝ) β†’ ℝhx:βˆ‘ v ∈ S, w v β€’ v ∈ (convexHull ℝ) ↑Shw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ (βˆ‘ x ∈ S, w x)⁻¹ β€’ βˆ‘ x ∈ S, w x β€’ x = βˆ‘ v ∈ S, w v β€’ vk:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝw:(Fin k β†’ ℝ) β†’ ℝhx:βˆ‘ v ∈ S, w v β€’ v ∈ (convexHull ℝ) ↑Shw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ βˆ€ x ∈ S, w x β€’ x β‰  0 β†’ Ο† x = Mk:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝw:(Fin k β†’ ℝ) β†’ ℝhx:βˆ‘ v ∈ S, w v β€’ v ∈ (convexHull ℝ) ↑Shw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ βˆ€ x ∈ S, w x β‰  0 β†’ Ο† x = M k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝw:(Fin k β†’ ℝ) β†’ ℝhx:βˆ‘ v ∈ S, w v β€’ v ∈ (convexHull ℝ) ↑Shw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ (βˆ‘ x ∈ S, w x)⁻¹ β€’ βˆ‘ x ∈ S, w x β€’ x = βˆ‘ v ∈ S, w v β€’ vk:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝw:(Fin k β†’ ℝ) β†’ ℝhx:βˆ‘ v ∈ S, w v β€’ v ∈ (convexHull ℝ) ↑Shw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ βˆ€ x ∈ S, w x β€’ x β‰  0 β†’ Ο† x = Mk:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝw:(Fin k β†’ ℝ) β†’ ℝhx:βˆ‘ v ∈ S, w v β€’ v ∈ (convexHull ℝ) ↑Shw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ βˆ€ x ∈ S, w x β‰  0 β†’ Ο† x = M k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝw:(Fin k β†’ ℝ) β†’ ℝhx:βˆ‘ v ∈ S, w v β€’ v ∈ (convexHull ℝ) ↑Shw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ βˆ€ x ∈ S, Β¬w x = 0 β†’ Ο† x = M; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝw:(Fin k β†’ ℝ) β†’ ℝhx:βˆ‘ v ∈ S, w v β€’ v ∈ (convexHull ℝ) ↑Shw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ βˆ€ x ∈ S, Β¬w x = 0 β†’ Β¬x = 0 β†’ Ο† x = M All goals completed! πŸ™; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝw:(Fin k β†’ ℝ) β†’ ℝhx:βˆ‘ v ∈ S, w v β€’ v ∈ (convexHull ℝ) ↑Shw:(βˆ€ v ∈ S, 0 ≀ w v) ∧ βˆ‘ v ∈ S, w v = 1 ∧ x = βˆ‘ v ∈ S, w v β€’ vh_sum:βˆ‘ v ∈ S, w v * Ο† v = Mh_zero:βˆ€ v ∈ S, Ο† v < M β†’ w v = 0⊒ βˆ€ x ∈ S, Β¬w x = 0 β†’ Ο† x = M All goals completed! πŸ™; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ (convexHull ℝ) ↑({v ∈ S | Ο† v = M})⊒ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ (convexHull ℝ) ↑({v ∈ S | Ο† v = M})⊒ ↑({v ∈ S | Ο† v = M}) βŠ† ↑Sk:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ (convexHull ℝ) ↑({v ∈ S | Ο† v = M})⊒ Ο† x = M; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ (convexHull ℝ) ↑({v ∈ S | Ο† v = M})⊒ ↑({v ∈ S | Ο† v = M}) βŠ† ↑S All goals completed! πŸ™; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ (convexHull ℝ) ↑({v ∈ S | Ο† v = M})⊒ Ο† x = M k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ Mx:Fin k β†’ ℝhx:x ∈ {x | βˆƒ ΞΉ t w z, (βˆ€ i ∈ t, 0 ≀ w i) ∧ βˆ‘ i ∈ t, w i = 1 ∧ (βˆ€ i ∈ t, z i ∈ ↑({v ∈ S | Ο† v = M})) ∧ t.centerMass w z = x}⊒ Ο† x = M; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typet:Finset ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhw₁:βˆ€ i ∈ t, 0 ≀ w ihwβ‚‚:βˆ‘ i ∈ t, w i = 1hw₃:βˆ€ i ∈ t, z i ∈ ↑({v ∈ S | Ο† v = M})⊒ Ο† (t.centerMass w z) = M; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MΞΉ:Typet:Finset ΞΉw:ΞΉ β†’ ℝz:ΞΉ β†’ Fin k β†’ ℝhw₁:βˆ€ i ∈ t, 0 ≀ w ihwβ‚‚:βˆ‘ i ∈ t, w i = 1hw₃:βˆ€ i ∈ t, z i ∈ S ∧ Ο† (z i) = M⊒ βˆ‘ x ∈ t, w x * M = M ; All goals completed! πŸ™ /- A linear functional that is constant `= M` on a set `T` is also constant `= M` on the whole affine span of `T` (an affine functional is determined affinely). -/ lemma eq_on_affineSpan_of_eq_on (Ο† : (Fin k β†’ ℝ) β†’β‚—[ℝ] ℝ) (M : ℝ) (T : Set (Fin k β†’ ℝ)) (hT : βˆ€ x ∈ T, Ο† x = M) : βˆ€ y ∈ affineSpan ℝ T, Ο† y = M := k:β„•Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝT:Set (Fin k β†’ ℝ)hT:βˆ€ x ∈ T, Ο† x = M⊒ βˆ€ y ∈ affineSpan ℝ T, Ο† y = M intro y k:β„•Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝT:Set (Fin k β†’ ℝ)hT:βˆ€ x ∈ T, Ο† x = My:Fin k β†’ ℝhy:y ∈ affineSpan ℝ T⊒ Ο† y = M; k:β„•Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝT:Set (Fin k β†’ ℝ)hT:βˆ€ x ∈ T, Ο† x = My:Fin k β†’ ℝy✝:Fin k β†’ ℝhys✝:y✝ ∈ T⊒ Ο† y✝ = Mk:β„•Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝT:Set (Fin k β†’ ℝ)hT:βˆ€ x ∈ T, Ο† x = My:Fin k β†’ ℝc✝:ℝu✝:Fin k β†’ ℝhu✝:u✝ ∈ affineSpan ℝ Tv✝:Fin k β†’ ℝhv✝:v✝ ∈ affineSpan ℝ Tw✝:Fin k β†’ ℝhw✝:w✝ ∈ affineSpan ℝ Ta✝²:Ο† u✝ = Ma✝¹:Ο† v✝ = Ma✝:Ο† w✝ = M⊒ Ο† (c✝ β€’ (u✝ -α΅₯ v✝) +α΅₯ w✝) = M ; k:β„•Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝT:Set (Fin k β†’ ℝ)hT:βˆ€ x ∈ T, Ο† x = My:Fin k β†’ ℝy✝:Fin k β†’ ℝhys✝:y✝ ∈ T⊒ Ο† y✝ = M All goals completed! πŸ™; k:β„•Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝT:Set (Fin k β†’ ℝ)hT:βˆ€ x ∈ T, Ο† x = My:Fin k β†’ ℝc✝:ℝu✝:Fin k β†’ ℝhu✝:u✝ ∈ affineSpan ℝ Tv✝:Fin k β†’ ℝhv✝:v✝ ∈ affineSpan ℝ Tw✝:Fin k β†’ ℝhw✝:w✝ ∈ affineSpan ℝ Ta✝²:Ο† u✝ = Ma✝¹:Ο† v✝ = Ma✝:Ο† w✝ = M⊒ Ο† (c✝ β€’ (u✝ -α΅₯ v✝) +α΅₯ w✝) = M All goals completed! πŸ™ /- A vertex strictly below the maximum value `M` is **not** in the affine span of the exposed face `{x | Ο† x = M}` of the polytope. This is exactly the hypothesis required by `coneComplex` / `coneSubdivision` to cone such a vertex over a far facet. -/ lemma notMem_affineSpan_exposedFace (S : Finset (Fin k β†’ ℝ)) (Ο† : (Fin k β†’ ℝ) β†’β‚—[ℝ] ℝ) (M : ℝ) (v : Fin k β†’ ℝ) (hv : Ο† v < M) : v βˆ‰ affineSpan ℝ {x ∈ convexHull ℝ (S : Set (Fin k β†’ ℝ)) | Ο† x = M} := k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝv:Fin k β†’ ℝhv:Ο† v < M⊒ v βˆ‰ affineSpan ℝ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝv:Fin k β†’ ℝhv:Ο† v < Mh:v ∈ affineSpan ℝ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}⊒ False; have h_affine_span : βˆ€ y ∈ affineSpan ℝ {x | x ∈ convexHull ℝ (S : Set (Fin k β†’ ℝ)) ∧ Ο† x = M}, Ο† y = M := k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝv:Fin k β†’ ℝhv:Ο† v < M⊒ v βˆ‰ affineSpan ℝ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝv:Fin k β†’ ℝhv:Ο† v < Mh:v ∈ affineSpan ℝ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}⊒ βˆ€ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M}, Ο† x = M; All goals completed! πŸ™; All goals completed! πŸ™ /- **Intersection of two exposed faces = exposed face of the sum.** If `M` (resp. `N`) is the maximum of `Ο†` (resp. `ψ`) over the polytope `convexHull S`, then the intersection of the two exposed faces is the convex hull of the vertices maximizing *both* functionals. This is the engine for the intersection (glue-nicely) property of a regular triangulation: every face there is an exposed face, and two exposed faces meet in the exposed face on their common maximizing vertices. -/ theorem exposedFace_inter_eq_convexHull_common_maximizers (S : Finset (Fin k β†’ ℝ)) (Ο† ψ : (Fin k β†’ ℝ) β†’β‚—[ℝ] ℝ) (M N : ℝ) (hM : βˆ€ v ∈ S, Ο† v ≀ M) (hN : βˆ€ v ∈ S, ψ v ≀ N) : {x ∈ convexHull ℝ (S : Set (Fin k β†’ ℝ)) | Ο† x = M} ∩ {x ∈ convexHull ℝ (S : Set (Fin k β†’ ℝ)) | ψ x = N} = convexHull ℝ ((S.filter (fun v => Ο† v = M ∧ ψ v = N) : Finset (Fin k β†’ ℝ)) : Set (Fin k β†’ ℝ)) := k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ N⊒ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} ∩ {x | x ∈ (convexHull ℝ) ↑S ∧ ψ x = N} = (convexHull ℝ) ↑({v ∈ S | Ο† v = M ∧ ψ v = N}) k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})⊒ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} ∩ {x | x ∈ (convexHull ℝ) ↑S ∧ ψ x = N} = (convexHull ℝ) ↑({v ∈ S | Ο† v = M ∧ ψ v = N}); k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})⊒ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} ∩ {x | x ∈ (convexHull ℝ) ↑S ∧ ψ x = N} = {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N}k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})⊒ (convexHull ℝ) ↑({v ∈ S | Ο† v = M ∧ ψ v = N}) = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N}); k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})⊒ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} ∩ {x | x ∈ (convexHull ℝ) ↑S ∧ ψ x = N} = {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})x:Fin k β†’ β„βŠ’ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} ∩ {x | x ∈ (convexHull ℝ) ↑S ∧ ψ x = N} ↔ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N}; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})x:Fin k β†’ β„βŠ’ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} ∩ {x | x ∈ (convexHull ℝ) ↑S ∧ ψ x = N} β†’ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N}k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})x:Fin k β†’ β„βŠ’ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} β†’ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} ∩ {x | x ∈ (convexHull ℝ) ↑S ∧ ψ x = N} k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})x:Fin k β†’ β„βŠ’ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} ∩ {x | x ∈ (convexHull ℝ) ↑S ∧ ψ x = N} β†’ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N}k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})x:Fin k β†’ β„βŠ’ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} β†’ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} ∩ {x | x ∈ (convexHull ℝ) ↑S ∧ ψ x = N} k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})x:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N}⊒ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} ∩ {x | x ∈ (convexHull ℝ) ↑S ∧ ψ x = N} k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})x:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} ∩ {x | x ∈ (convexHull ℝ) ↑S ∧ ψ x = N}⊒ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N}k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})x:Fin k β†’ ℝhx:x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N}⊒ x ∈ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} ∩ {x | x ∈ (convexHull ℝ) ↑S ∧ ψ x = N} k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nx:Fin k β†’ ℝineq:(βˆ€ v ∈ S, Ο† v + ψ v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x + ψ x = M + N} = (convexHull ℝ) {x | x ∈ S ∧ Ο† x + ψ x = M + N}hx:x ∈ (convexHull ℝ) ↑S ∧ Ο† x + ψ x = M + N⊒ Ο† x = M ∧ ψ x = N; have h_eq : βˆ€ x ∈ convexHull ℝ (S : Set (Fin k β†’ ℝ)), Ο† x ≀ M ∧ ψ x ≀ N := k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ N⊒ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x = M} ∩ {x | x ∈ (convexHull ℝ) ↑S ∧ ψ x = N} = (convexHull ℝ) ↑({v ∈ S | Ο† v = M ∧ ψ v = N}) All goals completed! πŸ™; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nx:Fin k β†’ ℝineq:(βˆ€ v ∈ S, Ο† v + ψ v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x + ψ x = M + N} = (convexHull ℝ) {x | x ∈ S ∧ Ο† x + ψ x = M + N}hx:x ∈ (convexHull ℝ) ↑S ∧ Ο† x + ψ x = M + Nh_eq:βˆ€ x ∈ (convexHull ℝ) ↑S, Ο† x ≀ M ∧ ψ x ≀ N⊒ Ο† x = Mk:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nx:Fin k β†’ ℝineq:(βˆ€ v ∈ S, Ο† v + ψ v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x + ψ x = M + N} = (convexHull ℝ) {x | x ∈ S ∧ Ο† x + ψ x = M + N}hx:x ∈ (convexHull ℝ) ↑S ∧ Ο† x + ψ x = M + Nh_eq:βˆ€ x ∈ (convexHull ℝ) ↑S, Ο† x ≀ M ∧ ψ x ≀ N⊒ ψ x = N k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nx:Fin k β†’ ℝineq:(βˆ€ v ∈ S, Ο† v + ψ v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x + ψ x = M + N} = (convexHull ℝ) {x | x ∈ S ∧ Ο† x + ψ x = M + N}hx:x ∈ (convexHull ℝ) ↑S ∧ Ο† x + ψ x = M + Nh_eq:βˆ€ x ∈ (convexHull ℝ) ↑S, Ο† x ≀ M ∧ ψ x ≀ N⊒ Ο† x = Mk:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nx:Fin k β†’ ℝineq:(βˆ€ v ∈ S, Ο† v + ψ v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ Ο† x + ψ x = M + N} = (convexHull ℝ) {x | x ∈ S ∧ Ο† x + ψ x = M + N}hx:x ∈ (convexHull ℝ) ↑S ∧ Ο† x + ψ x = M + Nh_eq:βˆ€ x ∈ (convexHull ℝ) ↑S, Ο† x ≀ M ∧ ψ x ≀ N⊒ ψ x = N All goals completed! πŸ™; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})⊒ (convexHull ℝ) ↑({v ∈ S | Ο† v = M ∧ ψ v = N}) = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N}) k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})⊒ {v ∈ S | Ο† v = M ∧ ψ v = N} = {v ∈ S | (Ο† + ψ) v = M + N}; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})v:Fin k β†’ β„βŠ’ v ∈ {v ∈ S | Ο† v = M ∧ ψ v = N} ↔ v ∈ {v ∈ S | (Ο† + ψ) v = M + N}; k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})v:Fin k β†’ β„βŠ’ v ∈ S β†’ (Ο† v = M ∧ ψ v = N ↔ Ο† v + ψ v = M + N); exact fun hv => ⟨ fun h => k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})v:Fin k β†’ ℝhv:v ∈ Sh:Ο† v = M ∧ ψ v = N⊒ Ο† v + ψ v = M + N All goals completed! πŸ™, fun h => ⟨ k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})v:Fin k β†’ ℝhv:v ∈ Sh:Ο† v + ψ v = M + N⊒ Ο† v = M All goals completed! πŸ™, k:β„•S:Finset (Fin k β†’ ℝ)Ο†:(Fin k β†’ ℝ) β†’β‚—[ℝ] β„Οˆ:(Fin k β†’ ℝ) β†’β‚—[ℝ] ℝM:ℝN:ℝhM:βˆ€ v ∈ S, Ο† v ≀ MhN:βˆ€ v ∈ S, ψ v ≀ Nineq:(βˆ€ v ∈ S, (Ο† + ψ) v ≀ M + N) β†’ {x | x ∈ (convexHull ℝ) ↑S ∧ (Ο† + ψ) x = M + N} = (convexHull ℝ) ↑({v ∈ S | (Ο† + ψ) v = M + N})v:Fin k β†’ ℝhv:v ∈ Sh:Ο† v + ψ v = M + N⊒ ψ v = N All goals completed! πŸ™ ⟩ ⟩ end FamiliesOfMapsB01Facets end Submission

Unions of simplicial complexesπŸ”—

From Union.lean: the union of two simplicial complexes is again a simplicial complex provided every cross pair of faces glues nicely β€” the missing primitive for assembling a triangulation from triangulated pieces.

open Geometry Set Finset open scoped Topology open _root_.FamiliesOfMapsB01 namespace Submission namespace FamiliesOfMapsB01 variable {k : β„•} /-- The face set of the union of `K₁` and `Kβ‚‚` (plus `βˆ…`, removed by `ofErase`). -/ def unionFaceSet (K₁ Kβ‚‚ : SimplicialComplex ℝ (Fin k β†’ ℝ)) : Set (Finset (Fin k β†’ ℝ)) := K₁.faces βˆͺ Kβ‚‚.faces βˆͺ {βˆ…} lemma unionFaceSet_indep (K₁ Kβ‚‚ : SimplicialComplex ℝ (Fin k β†’ ℝ)) : βˆ€ s ∈ unionFaceSet K₁ Kβ‚‚, AffineIndependent ℝ ((↑) : s β†’ (Fin k β†’ ℝ)) := k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)⊒ βˆ€ s ∈ unionFaceSet K₁ Kβ‚‚, AffineIndependent ℝ Subtype.val intro s k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)s:Finset (Fin k β†’ ℝ)hs:s ∈ unionFaceSet K₁ Kβ‚‚βŠ’ AffineIndependent ℝ Subtype.val k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)s:Finset (Fin k β†’ ℝ)hs:s ∈ K₁.faces⊒ AffineIndependent ℝ Subtype.valk:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)s:Finset (Fin k β†’ ℝ)hs:s ∈ Kβ‚‚.faces⊒ AffineIndependent ℝ Subtype.valk:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)s:Finset (Fin k β†’ ℝ)hs:s ∈ {βˆ…}⊒ AffineIndependent ℝ Subtype.val k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)s:Finset (Fin k β†’ ℝ)hs:s ∈ K₁.faces⊒ AffineIndependent ℝ Subtype.val All goals completed! πŸ™ k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)s:Finset (Fin k β†’ ℝ)hs:s ∈ Kβ‚‚.faces⊒ AffineIndependent ℝ Subtype.val All goals completed! πŸ™ k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)s:Finset (Fin k β†’ ℝ)hs:s ∈ {βˆ…}⊒ AffineIndependent ℝ Subtype.val k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)s:Finset (Fin k β†’ ℝ)hs:s = βˆ…βŠ’ AffineIndependent ℝ Subtype.val k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)⊒ AffineIndependent ℝ Subtype.val All goals completed! πŸ™ lemma unionFaceSet_isLowerSet (K₁ Kβ‚‚ : SimplicialComplex ℝ (Fin k β†’ ℝ)) : IsLowerSet (unionFaceSet K₁ Kβ‚‚) := k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)⊒ IsLowerSet (unionFaceSet K₁ Kβ‚‚) intro a k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)a:Finset (Fin k β†’ ℝ)b:Finset (Fin k β†’ ℝ)⊒ b ≀ a β†’ a ∈ unionFaceSet K₁ Kβ‚‚ β†’ b ∈ unionFaceSet K₁ Kβ‚‚ k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)a:Finset (Fin k β†’ ℝ)b:Finset (Fin k β†’ ℝ)hab:b ≀ a⊒ a ∈ unionFaceSet K₁ Kβ‚‚ β†’ b ∈ unionFaceSet K₁ Kβ‚‚ k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)a:Finset (Fin k β†’ ℝ)b:Finset (Fin k β†’ ℝ)hab:b ≀ aha:a ∈ unionFaceSet K₁ Kβ‚‚βŠ’ b ∈ unionFaceSet K₁ Kβ‚‚ k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)a:Finset (Fin k β†’ ℝ)b:Finset (Fin k β†’ ℝ)hab:b ≀ aha:(a ∈ K₁.faces ∨ a ∈ Kβ‚‚.faces) ∨ a = βˆ…βŠ’ (b ∈ K₁.faces ∨ b ∈ Kβ‚‚.faces) ∨ b = βˆ… k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)a:Finset (Fin k β†’ ℝ)b:Finset (Fin k β†’ ℝ)hab:b ≀ aha:(a ∈ K₁.faces ∨ a ∈ Kβ‚‚.faces) ∨ a = βˆ…hbe:b = βˆ…βŠ’ (b ∈ K₁.faces ∨ b ∈ Kβ‚‚.faces) ∨ b = βˆ…k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)a:Finset (Fin k β†’ ℝ)b:Finset (Fin k β†’ ℝ)hab:b ≀ aha:(a ∈ K₁.faces ∨ a ∈ Kβ‚‚.faces) ∨ a = βˆ…hbe:Β¬b = βˆ…βŠ’ (b ∈ K₁.faces ∨ b ∈ Kβ‚‚.faces) ∨ b = βˆ… k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)a:Finset (Fin k β†’ ℝ)b:Finset (Fin k β†’ ℝ)hab:b ≀ aha:(a ∈ K₁.faces ∨ a ∈ Kβ‚‚.faces) ∨ a = βˆ…hbe:b = βˆ…βŠ’ (b ∈ K₁.faces ∨ b ∈ Kβ‚‚.faces) ∨ b = βˆ… All goals completed! πŸ™ k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)a:Finset (Fin k β†’ ℝ)b:Finset (Fin k β†’ ℝ)hab:b ≀ aha:(a ∈ K₁.faces ∨ a ∈ Kβ‚‚.faces) ∨ a = βˆ…hbe:Β¬b = βˆ…βŠ’ (b ∈ K₁.faces ∨ b ∈ Kβ‚‚.faces) ∨ b = βˆ… k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)a:Finset (Fin k β†’ ℝ)b:Finset (Fin k β†’ ℝ)hab:b ≀ aha:(a ∈ K₁.faces ∨ a ∈ Kβ‚‚.faces) ∨ a = βˆ…hbe:Β¬b = βˆ…hbne:b.Nonempty⊒ (b ∈ K₁.faces ∨ b ∈ Kβ‚‚.faces) ∨ b = βˆ… k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)a:Finset (Fin k β†’ ℝ)b:Finset (Fin k β†’ ℝ)hab:b ≀ aha:(a ∈ K₁.faces ∨ a ∈ Kβ‚‚.faces) ∨ a = βˆ…hbe:Β¬b = βˆ…hbne:b.Nonemptyhba:b βŠ† a⊒ (b ∈ K₁.faces ∨ b ∈ Kβ‚‚.faces) ∨ b = βˆ… k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)a:Finset (Fin k β†’ ℝ)b:Finset (Fin k β†’ ℝ)hab:b ≀ ahbe:Β¬b = βˆ…hbne:b.Nonemptyhba:b βŠ† aha:a ∈ K₁.faces⊒ (b ∈ K₁.faces ∨ b ∈ Kβ‚‚.faces) ∨ b = βˆ…k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)a:Finset (Fin k β†’ ℝ)b:Finset (Fin k β†’ ℝ)hab:b ≀ ahbe:Β¬b = βˆ…hbne:b.Nonemptyhba:b βŠ† aha:a ∈ Kβ‚‚.faces⊒ (b ∈ K₁.faces ∨ b ∈ Kβ‚‚.faces) ∨ b = βˆ…k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)a:Finset (Fin k β†’ ℝ)b:Finset (Fin k β†’ ℝ)hab:b ≀ ahbe:Β¬b = βˆ…hbne:b.Nonemptyhba:b βŠ† aha:a = βˆ…βŠ’ (b ∈ K₁.faces ∨ b ∈ Kβ‚‚.faces) ∨ b = βˆ… k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)a:Finset (Fin k β†’ ℝ)b:Finset (Fin k β†’ ℝ)hab:b ≀ ahbe:Β¬b = βˆ…hbne:b.Nonemptyhba:b βŠ† aha:a ∈ K₁.faces⊒ (b ∈ K₁.faces ∨ b ∈ Kβ‚‚.faces) ∨ b = βˆ… All goals completed! πŸ™ k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)a:Finset (Fin k β†’ ℝ)b:Finset (Fin k β†’ ℝ)hab:b ≀ ahbe:Β¬b = βˆ…hbne:b.Nonemptyhba:b βŠ† aha:a ∈ Kβ‚‚.faces⊒ (b ∈ K₁.faces ∨ b ∈ Kβ‚‚.faces) ∨ b = βˆ… All goals completed! πŸ™ k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)a:Finset (Fin k β†’ ℝ)b:Finset (Fin k β†’ ℝ)hab:b ≀ ahbe:Β¬b = βˆ…hbne:b.Nonemptyhba:b βŠ† aha:a = βˆ…βŠ’ (b ∈ K₁.faces ∨ b ∈ Kβ‚‚.faces) ∨ b = βˆ… k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)b:Finset (Fin k β†’ ℝ)hbe:Β¬b = βˆ…hbne:b.Nonemptyhab:b ≀ βˆ…hba:b βŠ† βˆ…βŠ’ (b ∈ K₁.faces ∨ b ∈ Kβ‚‚.faces) ∨ b = βˆ… All goals completed! πŸ™ /-- The cross-gluing hypothesis: every face of `K₁` and every face of `Kβ‚‚` meet nicely. This is what makes the union a simplicial complex. -/ def UnionGlues (K₁ Kβ‚‚ : SimplicialComplex ℝ (Fin k β†’ ℝ)) : Prop := βˆ€ s ∈ K₁.faces, βˆ€ t ∈ Kβ‚‚.faces, convexHull ℝ (s : Set (Fin k β†’ ℝ)) ∩ convexHull ℝ (t : Set (Fin k β†’ ℝ)) βŠ† convexHull ℝ ((s : Set (Fin k β†’ ℝ)) ∩ (t : Set (Fin k β†’ ℝ))) lemma unionFaceSet_inter (K₁ Kβ‚‚ : SimplicialComplex ℝ (Fin k β†’ ℝ)) (hglue : UnionGlues K₁ Kβ‚‚) : βˆ€ s ∈ unionFaceSet K₁ Kβ‚‚, βˆ€ t ∈ unionFaceSet K₁ Kβ‚‚, convexHull ℝ (s : Set (Fin k β†’ ℝ)) ∩ convexHull ℝ (t : Set (Fin k β†’ ℝ)) βŠ† convexHull ℝ ((s : Set (Fin k β†’ ℝ)) ∩ (t : Set (Fin k β†’ ℝ))) := k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚βŠ’ βˆ€ s ∈ unionFaceSet K₁ Kβ‚‚, βˆ€ t ∈ unionFaceSet K₁ Kβ‚‚, (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t) intro s k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)hs:s ∈ unionFaceSet K₁ Kβ‚‚βŠ’ βˆ€ t ∈ unionFaceSet K₁ Kβ‚‚, (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t) k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)hs:s ∈ unionFaceSet K₁ Kβ‚‚t:Finset (Fin k β†’ ℝ)⊒ t ∈ unionFaceSet K₁ Kβ‚‚ β†’ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t) k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)hs:s ∈ unionFaceSet K₁ Kβ‚‚t:Finset (Fin k β†’ ℝ)ht:t ∈ unionFaceSet K₁ Kβ‚‚βŠ’ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t) -- Empty cases are trivial since convexHull of βˆ… is βˆ…. k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)ht:t ∈ unionFaceSet K₁ Kβ‚‚hs:s ∈ K₁.faces⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t)k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)ht:t ∈ unionFaceSet K₁ Kβ‚‚hs:s ∈ Kβ‚‚.faces⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t)k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)ht:t ∈ unionFaceSet K₁ Kβ‚‚hs:s ∈ {βˆ…}⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t) k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)ht:t ∈ unionFaceSet K₁ Kβ‚‚hs:s ∈ K₁.faces⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t) k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)hs:s ∈ K₁.facesht:t ∈ K₁.faces⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t)k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)hs:s ∈ K₁.facesht:t ∈ Kβ‚‚.faces⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t)k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)hs:s ∈ K₁.facesht:t ∈ {βˆ…}⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t) k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)hs:s ∈ K₁.facesht:t ∈ K₁.faces⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t) All goals completed! πŸ™ k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)hs:s ∈ K₁.facesht:t ∈ Kβ‚‚.faces⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t) All goals completed! πŸ™ k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)hs:s ∈ K₁.facesht:t ∈ {βˆ…}⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t) k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)hs:s ∈ K₁.facesht:t = βˆ…βŠ’ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t); k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)hs:s ∈ K₁.faces⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) β†‘βˆ… βŠ† (convexHull ℝ) (↑s ∩ β†‘βˆ…); All goals completed! πŸ™ k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)ht:t ∈ unionFaceSet K₁ Kβ‚‚hs:s ∈ Kβ‚‚.faces⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t) k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)hs:s ∈ Kβ‚‚.facesht:t ∈ K₁.faces⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t)k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)hs:s ∈ Kβ‚‚.facesht:t ∈ Kβ‚‚.faces⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t)k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)hs:s ∈ Kβ‚‚.facesht:t ∈ {βˆ…}⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t) k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)hs:s ∈ Kβ‚‚.facesht:t ∈ K₁.faces⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t) intro x k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)hs:s ∈ Kβ‚‚.facesht:t ∈ K₁.facesx:Fin k β†’ ℝhx:x ∈ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t⊒ x ∈ (convexHull ℝ) (↑s ∩ ↑t) k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)hs:s ∈ Kβ‚‚.facesht:t ∈ K₁.facesx:Fin k β†’ ℝhx:x ∈ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑tthis:x ∈ (convexHull ℝ) (↑t ∩ ↑s)⊒ x ∈ (convexHull ℝ) (↑s ∩ ↑t) k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)hs:s ∈ Kβ‚‚.facesht:t ∈ K₁.facesx:Fin k β†’ ℝhx:x ∈ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑tthis:x ∈ (convexHull ℝ) (↑s ∩ ↑t)⊒ x ∈ (convexHull ℝ) (↑s ∩ ↑t) All goals completed! πŸ™ k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)hs:s ∈ Kβ‚‚.facesht:t ∈ Kβ‚‚.faces⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t) All goals completed! πŸ™ k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)hs:s ∈ Kβ‚‚.facesht:t ∈ {βˆ…}⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t) k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)hs:s ∈ Kβ‚‚.facesht:t = βˆ…βŠ’ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t); k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)hs:s ∈ Kβ‚‚.faces⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) β†‘βˆ… βŠ† (convexHull ℝ) (↑s ∩ β†‘βˆ…); All goals completed! πŸ™ k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)ht:t ∈ unionFaceSet K₁ Kβ‚‚hs:s ∈ {βˆ…}⊒ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t) k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚s:Finset (Fin k β†’ ℝ)t:Finset (Fin k β†’ ℝ)ht:t ∈ unionFaceSet K₁ Kβ‚‚hs:s = βˆ…βŠ’ (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (↑s ∩ ↑t); k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚t:Finset (Fin k β†’ ℝ)ht:t ∈ unionFaceSet K₁ Kβ‚‚βŠ’ (convexHull ℝ) β†‘βˆ… ∩ (convexHull ℝ) ↑t βŠ† (convexHull ℝ) (β†‘βˆ… ∩ ↑t); All goals completed! πŸ™ /-- The **union (gluing) of two simplicial complexes** `K₁`, `Kβ‚‚`, valid whenever every cross pair of faces glues nicely (`UnionGlues`). -/ noncomputable def unionComplex (K₁ Kβ‚‚ : SimplicialComplex ℝ (Fin k β†’ ℝ)) (hglue : UnionGlues K₁ Kβ‚‚) : SimplicialComplex ℝ (Fin k β†’ ℝ) := SimplicialComplex.ofErase (unionFaceSet K₁ Kβ‚‚) (unionFaceSet_indep K₁ Kβ‚‚) (unionFaceSet_isLowerSet K₁ Kβ‚‚) (unionFaceSet_inter K₁ Kβ‚‚ hglue) lemma unionComplex_faces (K₁ Kβ‚‚ : SimplicialComplex ℝ (Fin k β†’ ℝ)) (hglue : UnionGlues K₁ Kβ‚‚) : (unionComplex K₁ Kβ‚‚ hglue).faces = unionFaceSet K₁ Kβ‚‚ \ {βˆ…} := k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚βŠ’ (unionComplex K₁ Kβ‚‚ hglue).faces = unionFaceSet K₁ Kβ‚‚ \ {βˆ…} All goals completed! πŸ™ /- The space of the union is the union of the spaces. -/ lemma unionComplex_space (K₁ Kβ‚‚ : SimplicialComplex ℝ (Fin k β†’ ℝ)) (hglue : UnionGlues K₁ Kβ‚‚) : (unionComplex K₁ Kβ‚‚ hglue).space = K₁.space βˆͺ Kβ‚‚.space := k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚βŠ’ (unionComplex K₁ Kβ‚‚ hglue).space = K₁.space βˆͺ Kβ‚‚.space k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚x:Fin k β†’ β„βŠ’ x ∈ (unionComplex K₁ Kβ‚‚ hglue).space ↔ x ∈ K₁.space βˆͺ Kβ‚‚.space k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚x:Fin k β†’ β„βŠ’ (βˆƒ s, ((s ∈ K₁.faces ∨ s ∈ Kβ‚‚.faces) ∧ Β¬s = βˆ…) ∧ x ∈ (convexHull ℝ) ↑s) ↔ (βˆƒ s ∈ K₁.faces, x ∈ (convexHull ℝ) ↑s) ∨ βˆƒ s ∈ Kβ‚‚.faces, x ∈ (convexHull ℝ) ↑s; k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚x:Fin k β†’ β„βŠ’ (βˆƒ s, ((s ∈ K₁.faces ∨ s ∈ Kβ‚‚.faces) ∧ Β¬s = βˆ…) ∧ x ∈ (convexHull ℝ) ↑s) β†’ (βˆƒ s ∈ K₁.faces, x ∈ (convexHull ℝ) ↑s) ∨ βˆƒ s ∈ Kβ‚‚.faces, x ∈ (convexHull ℝ) ↑sk:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚x:Fin k β†’ β„βŠ’ ((βˆƒ s ∈ K₁.faces, x ∈ (convexHull ℝ) ↑s) ∨ βˆƒ s ∈ Kβ‚‚.faces, x ∈ (convexHull ℝ) ↑s) β†’ βˆƒ s, ((s ∈ K₁.faces ∨ s ∈ Kβ‚‚.faces) ∧ Β¬s = βˆ…) ∧ x ∈ (convexHull ℝ) ↑s; k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚x:Fin k β†’ β„βŠ’ (βˆƒ s, ((s ∈ K₁.faces ∨ s ∈ Kβ‚‚.faces) ∧ Β¬s = βˆ…) ∧ x ∈ (convexHull ℝ) ↑s) β†’ (βˆƒ s ∈ K₁.faces, x ∈ (convexHull ℝ) ↑s) ∨ βˆƒ s ∈ Kβ‚‚.faces, x ∈ (convexHull ℝ) ↑s All goals completed! πŸ™; k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚x:Fin k β†’ β„βŠ’ ((βˆƒ s ∈ K₁.faces, x ∈ (convexHull ℝ) ↑s) ∨ βˆƒ s ∈ Kβ‚‚.faces, x ∈ (convexHull ℝ) ↑s) β†’ βˆƒ s, ((s ∈ K₁.faces ∨ s ∈ Kβ‚‚.faces) ∧ Β¬s = βˆ…) ∧ x ∈ (convexHull ℝ) ↑s k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚x:Fin k β†’ ℝs:Finset (Fin k β†’ ℝ)hs₁:s ∈ K₁.faceshsβ‚‚:x ∈ (convexHull ℝ) ↑s⊒ βˆƒ s, ((s ∈ K₁.faces ∨ s ∈ Kβ‚‚.faces) ∧ Β¬s = βˆ…) ∧ x ∈ (convexHull ℝ) ↑sk:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚x:Fin k β†’ ℝs:Finset (Fin k β†’ ℝ)hs₁:s ∈ Kβ‚‚.faceshsβ‚‚:x ∈ (convexHull ℝ) ↑s⊒ βˆƒ s, ((s ∈ K₁.faces ∨ s ∈ Kβ‚‚.faces) ∧ Β¬s = βˆ…) ∧ x ∈ (convexHull ℝ) ↑s <;> [ exact ⟨ s, ⟨ Or.inl hs₁, k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚x:Fin k β†’ ℝs:Finset (Fin k β†’ ℝ)hs₁:s ∈ K₁.faceshsβ‚‚:x ∈ (convexHull ℝ) ↑s⊒ Β¬s = βˆ… k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚x:Fin k β†’ ℝhs₁:βˆ… ∈ K₁.faceshsβ‚‚:x ∈ (convexHull ℝ) β†‘βˆ…βŠ’ False; All goals completed! πŸ™ ⟩, hsβ‚‚ ⟩ ; exact ⟨ s, ⟨ Or.inr hs₁, k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚x:Fin k β†’ ℝs:Finset (Fin k β†’ ℝ)hs₁:s ∈ Kβ‚‚.faceshsβ‚‚:x ∈ (convexHull ℝ) ↑s⊒ Β¬s = βˆ… k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚x:Fin k β†’ ℝhs₁:βˆ… ∈ Kβ‚‚.faceshsβ‚‚:x ∈ (convexHull ℝ) β†‘βˆ…βŠ’ False; All goals completed! πŸ™ ⟩, hsβ‚‚ ⟩ ] lemma unionComplex_faces_finite (K₁ Kβ‚‚ : SimplicialComplex ℝ (Fin k β†’ ℝ)) (hglue : UnionGlues K₁ Kβ‚‚) (h₁ : K₁.faces.Finite) (hβ‚‚ : Kβ‚‚.faces.Finite) : (unionComplex K₁ Kβ‚‚ hglue).faces.Finite := k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚h₁:K₁.faces.Finitehβ‚‚:Kβ‚‚.faces.Finite⊒ (unionComplex K₁ Kβ‚‚ hglue).faces.Finite k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚h₁:K₁.faces.Finitehβ‚‚:Kβ‚‚.faces.Finite⊒ (unionComplex K₁ Kβ‚‚ hglue).faces βŠ† K₁.faces βˆͺ (Kβ‚‚.faces βˆͺ {βˆ…}); k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚h₁:K₁.faces.Finitehβ‚‚:Kβ‚‚.faces.Finite⊒ unionFaceSet K₁ Kβ‚‚ βŠ† insert βˆ… (K₁.faces βˆͺ Kβ‚‚.faces); exact fun x hx => k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚h₁:K₁.faces.Finitehβ‚‚:Kβ‚‚.faces.Finitex:Finset (Fin k β†’ ℝ)hx:x ∈ unionFaceSet K₁ Kβ‚‚βŠ’ x ∈ insert βˆ… (K₁.faces βˆͺ Kβ‚‚.faces) k:β„•K₁:SimplicialComplex ℝ (Fin k β†’ ℝ)Kβ‚‚:SimplicialComplex ℝ (Fin k β†’ ℝ)hglue:UnionGlues K₁ Kβ‚‚h₁:K₁.faces.Finitehβ‚‚:Kβ‚‚.faces.Finitex:Finset (Fin k β†’ ℝ)hx:x ∈ K₁.faces βˆͺ Kβ‚‚.faces βˆͺ {βˆ…}⊒ x ∈ insert βˆ… (K₁.faces βˆͺ Kβ‚‚.faces); All goals completed! πŸ™; end FamiliesOfMapsB01 end Submission

Continuity of a single affine realizationπŸ”—

From Collapse.lean: the affine extension over a single simplex, via barycentric coordinates of an affine basis, is continuous. (The realization actually used is glued from prescribed-value affine maps instead; see the realization chapter.)

open Set Finset open scoped Topology BigOperators namespace Submission namespace FamiliesOfMapsB01Collapse variable {k : β„•} /- The affine extension over a single affinely-independent simplex is continuous: for an `AffineBasis` `b` of (the affine span of) a simplex and any target assignment `g : ΞΉ β†’ ℝᡏ`, the map `q ↦ Ξ£_i (b.coord i q) β€’ g i` is continuous. -/ lemma continuous_affine_realization {ΞΉ : Type*} [Fintype ΞΉ] (b : AffineBasis ΞΉ ℝ (Fin k β†’ ℝ)) (g : ΞΉ β†’ (Fin k β†’ ℝ)) : Continuous (fun q : (Fin k β†’ ℝ) => βˆ‘ i, (b.coord i q) β€’ g i) := k:β„•ΞΉ:Type u_1inst✝:Fintype ΞΉb:AffineBasis ΞΉ ℝ (Fin k β†’ ℝ)g:ΞΉ β†’ Fin k β†’ β„βŠ’ Continuous fun q => βˆ‘ i, (b.coord i) q β€’ g i k:β„•ΞΉ:Type u_1inst✝:Fintype ΞΉb:AffineBasis ΞΉ ℝ (Fin k β†’ ℝ)g:ΞΉ β†’ Fin k β†’ β„βŠ’ ContinuousAdd (Fin k β†’ ℝ)k:β„•ΞΉ:Type u_1inst✝:Fintype ΞΉb:AffineBasis ΞΉ ℝ (Fin k β†’ ℝ)g:ΞΉ β†’ Fin k β†’ β„βŠ’ βˆ€ i ∈ Finset.univ, ContinuousSMul ℝ (Fin k β†’ ℝ); k:β„•ΞΉ:Type u_1inst✝:Fintype ΞΉb:AffineBasis ΞΉ ℝ (Fin k β†’ ℝ)g:ΞΉ β†’ Fin k β†’ β„βŠ’ ContinuousAdd (Fin k β†’ ℝ) All goals completed! πŸ™; k:β„•ΞΉ:Type u_1inst✝:Fintype ΞΉb:AffineBasis ΞΉ ℝ (Fin k β†’ ℝ)g:ΞΉ β†’ Fin k β†’ β„βŠ’ βˆ€ i ∈ Finset.univ, ContinuousSMul ℝ (Fin k β†’ ℝ) All goals completed! πŸ™ end FamiliesOfMapsB01Collapse end Submission

At most one extreme point per barycentric faceπŸ”—

From Fineness.lean: the centroid of a face with at least two vertices is never an extreme point, and a barycentric face contains at most one extreme point of P β€” a fineness property that the quantile construction's mesh-based argument ended up not needing.

open Geometry Set open scoped BigOperators Classical open _root_.FamiliesOfMapsB01 open Submission.FamiliesOfMapsB01Bary namespace Submission namespace FamiliesOfMapsB01 variable {k : β„•} /- The centroid of a face with at least two vertices is **not** an extreme point of any convex set `P` containing the face: it is a convex combination, with strictly positive weights, of two distinct points of `P`. -/ lemma centroid_not_extreme_of_card_ge_two {P : Set (Fin k β†’ ℝ)} (hPconv : Convex ℝ P) {Οƒ : Finset (Fin k β†’ ℝ)} (hΟƒP : (Οƒ : Set (Fin k β†’ ℝ)) βŠ† P) (hcard : 2 ≀ Οƒ.card) (hindep : AffineIndependent ℝ ((↑) : Οƒ β†’ (Fin k β†’ ℝ))) : Finset.centroid ℝ Οƒ id βˆ‰ Set.extremePoints ℝ P := k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.val⊒ centroid ℝ Οƒ id βˆ‰ extremePoints ℝ P k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ P⊒ False; -- Write c = weighted average of q andcentroid(Οƒ.erase q), both ∈ P, with strictly positive weights. Let q be any vertex of Οƒ. obtain ⟨q, hq⟩ : βˆƒ q ∈ Οƒ, q β‰  Finset.centroid ℝ (Οƒ.erase q) id := k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ P⊒ βˆƒ q ∈ Οƒ, q β‰  centroid ℝ (Οƒ.erase q) id k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) id⊒ Β¬AffineIndependent ℝ Subtype.val; -- If every vertex of Οƒ is equal to the centroid of the rest, then Οƒ is a degenerate simplex. have h_degenerate : βˆ€ q ∈ Οƒ, q = Finset.centroid ℝ Οƒ id := k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ P⊒ βˆƒ q ∈ Οƒ, q β‰  centroid ℝ (Οƒ.erase q) id intro q k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idq:Fin k β†’ ℝhq:q ∈ ΟƒβŠ’ q = centroid ℝ Οƒ id k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idq:Fin k β†’ ℝhq:q ∈ Οƒh_eq:q = centroid ℝ (Οƒ.erase q) id⊒ q = centroid ℝ Οƒ id have h_eq' : Finset.centroid ℝ Οƒ id = (1 / Οƒ.card : ℝ) β€’ q + ((Οƒ.card - 1) / Οƒ.card : ℝ) β€’ Finset.centroid ℝ (Οƒ.erase q) id := k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ P⊒ βˆƒ q ∈ Οƒ, q β‰  centroid ℝ (Οƒ.erase q) id k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idq:Fin k β†’ ℝhq:q ∈ Οƒh_eq:q = centroid ℝ (Οƒ.erase q) id⊒ (affineCombination ℝ Οƒ id) (centroidWeights ℝ Οƒ) = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ (affineCombination ℝ (Οƒ.erase q) id) (centroidWeights ℝ (Οƒ.erase q)); k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idq:Fin k β†’ ℝhq:q ∈ Οƒh_eq:q = centroid ℝ (Οƒ.erase q) id⊒ βˆ‘ i ∈ Οƒ, centroidWeights ℝ Οƒ i β€’ id i = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ βˆ‘ i ∈ Οƒ.erase q, centroidWeights ℝ (Οƒ.erase q) i β€’ id ik:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idq:Fin k β†’ ℝhq:q ∈ Οƒh_eq:q = centroid ℝ (Οƒ.erase q) id⊒ βˆ‘ i ∈ Οƒ.erase q, centroidWeights ℝ (Οƒ.erase q) i = 1k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idq:Fin k β†’ ℝhq:q ∈ Οƒh_eq:q = centroid ℝ (Οƒ.erase q) id⊒ βˆ‘ i ∈ Οƒ, centroidWeights ℝ Οƒ i = 1; k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idq:Fin k β†’ ℝhq:q ∈ Οƒh_eq:q = centroid ℝ (Οƒ.erase q) id⊒ βˆ‘ i ∈ Οƒ, centroidWeights ℝ Οƒ i β€’ id i = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ βˆ‘ i ∈ Οƒ.erase q, centroidWeights ℝ (Οƒ.erase q) i β€’ id i k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idq:Fin k β†’ ℝhq:q ∈ Οƒh_eq:q = centroid ℝ (Οƒ.erase q) id⊒ centroidWeights ℝ (insert q (Οƒ.erase q)) q β€’ id q + βˆ‘ x ∈ Οƒ.erase q, centroidWeights ℝ (insert q (Οƒ.erase q)) x β€’ id x = (1 / ↑(#(insert q (Οƒ.erase q)))) β€’ q + ((↑(#(insert q (Οƒ.erase q))) - 1) / ↑(#(insert q (Οƒ.erase q)))) β€’ βˆ‘ i ∈ (insert q (Οƒ.erase q)).erase q, centroidWeights ℝ ((insert q (Οƒ.erase q)).erase q) i β€’ id i ; k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idq:Fin k β†’ ℝhq:q ∈ Οƒh_eq:q = centroid ℝ (Οƒ.erase q) id⊒ βˆ‘ x ∈ Οƒ.erase q, (↑(#Οƒ - 1) + 1)⁻¹ β€’ x = (↑(#Οƒ - 1) / (↑(#Οƒ - 1) + 1)) β€’ βˆ‘ x ∈ Οƒ.erase q, (↑(#Οƒ - 1))⁻¹ β€’ x ; Try this: [apply] ring_nf The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form. Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idq:Fin k β†’ ℝhq:q ∈ Οƒh_eq:q = centroid ℝ (Οƒ.erase q) id⊒ βˆ‘ x ∈ Οƒ.erase q, (1 + ↑(#Οƒ - 1))⁻¹ β€’ x = (↑(#Οƒ - 1) * (1 + ↑(#Οƒ - 1))⁻¹) β€’ βˆ‘ x ∈ Οƒ.erase q, (↑(#Οƒ - 1))⁻¹ β€’ x; All goals completed! πŸ™; k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idq:Fin k β†’ ℝhq:q ∈ Οƒh_eq:q = centroid ℝ (Οƒ.erase q) id⊒ βˆ‘ i ∈ Οƒ.erase q, centroidWeights ℝ (Οƒ.erase q) i = 1 k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idq:Fin k β†’ ℝhq:q ∈ Οƒh_eq:q = centroid ℝ (Οƒ.erase q) id⊒ ↑(#Οƒ - 1) * (↑(#Οƒ - 1))⁻¹ = 1; All goals completed! πŸ™; k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idq:Fin k β†’ ℝhq:q ∈ Οƒh_eq:q = centroid ℝ (Οƒ.erase q) id⊒ βˆ‘ i ∈ Οƒ, centroidWeights ℝ Οƒ i = 1 All goals completed! πŸ™; k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idq:Fin k β†’ ℝhq:q ∈ Οƒh_eq:q = centroid ℝ (Οƒ.erase q) idh_eq':centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ q = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ q; k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idq:Fin k β†’ ℝhq:q ∈ Οƒh_eq:q = centroid ℝ (Οƒ.erase q) idh_eq':centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ q = (1 / ↑(#Οƒ) + (↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ q ; k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idq:Fin k β†’ ℝhq:q ∈ Οƒh_eq:q = centroid ℝ (Οƒ.erase q) idh_eq':centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ q = (↑(#Οƒ) * (↑(#Οƒ))⁻¹) β€’ q ; norm_num [ show Οƒ.card β‰  0 k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ P⊒ βˆƒ q ∈ Οƒ, q β‰  centroid ℝ (Οƒ.erase q) id All goals completed! πŸ™ ]; exact absurd ( Finset.card_le_one.mpr fun x hx y hy => k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idh_degenerate:βˆ€ q ∈ Οƒ, q = centroid ℝ Οƒ idx:?m.245hx:x ∈ ?m.246y:?m.245hy:y ∈ ?m.246⊒ x = y All goals completed! πŸ™ ) ( k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒh:centroid ℝ Οƒ id ∈ extremePoints ℝ Phindep:βˆ€ q ∈ Οƒ, q = centroid ℝ (Οƒ.erase q) idh_degenerate:βˆ€ q ∈ Οƒ, q = centroid ℝ Οƒ id⊒ Β¬#Οƒ ≀ 1 All goals completed! πŸ™ ); have h_convex_comb : Finset.centroid ℝ Οƒ id = (1 / Οƒ.card : ℝ) β€’ q + ((Οƒ.card - 1) / Οƒ.card : ℝ) β€’ Finset.centroid ℝ (Οƒ.erase q) id := k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.val⊒ centroid ℝ Οƒ id βˆ‰ extremePoints ℝ P k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) id⊒ (affineCombination ℝ Οƒ id) (centroidWeights ℝ Οƒ) = (↑(#Οƒ))⁻¹ β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ (affineCombination ℝ (Οƒ.erase q) id) (centroidWeights ℝ (Οƒ.erase q)); k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) id⊒ βˆ‘ x ∈ Οƒ, (↑(#Οƒ))⁻¹ β€’ (x - Classical.choice β‹―) + Classical.choice β‹― = (↑(#Οƒ))⁻¹ β€’ q + (((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ (βˆ‘ x ∈ Οƒ, (↑(#Οƒ - 1))⁻¹ β€’ (x - Classical.choice β‹―) - (↑(#Οƒ - 1))⁻¹ β€’ (q - Classical.choice β‹―)) + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ Classical.choice β‹―); k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) id⊒ (↑(#Οƒ))⁻¹ β€’ (βˆ‘ x ∈ Οƒ, x - ↑(#Οƒ) * Classical.choice β‹―) + Classical.choice β‹― = (↑(#Οƒ))⁻¹ β€’ q + ((1 - (↑(#Οƒ))⁻¹) β€’ ((↑(#Οƒ) - 1)⁻¹ β€’ (βˆ‘ x ∈ Οƒ, x - ↑(#Οƒ) * Classical.choice β‹―) - (↑(#Οƒ) - 1)⁻¹ β€’ (q - Classical.choice β‹―)) + (1 - (↑(#Οƒ))⁻¹) β€’ Classical.choice β‹―); k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) id⊒ (↑(#Οƒ))⁻¹ β€’ βˆ‘ x ∈ Οƒ, x - (↑(#Οƒ))⁻¹ β€’ (↑(#Οƒ) * Classical.choice β‹―) + Classical.choice β‹― = (↑(#Οƒ))⁻¹ β€’ q + (((1 - (↑(#Οƒ))⁻¹) * (↑(#Οƒ) - 1)⁻¹) β€’ βˆ‘ x ∈ Οƒ, x - ((1 - (↑(#Οƒ))⁻¹) * (↑(#Οƒ) - 1)⁻¹) β€’ (↑(#Οƒ) * Classical.choice β‹―) - (((1 - (↑(#Οƒ))⁻¹) * (↑(#Οƒ) - 1)⁻¹) β€’ q - ((1 - (↑(#Οƒ))⁻¹) * (↑(#Οƒ) - 1)⁻¹) β€’ Classical.choice β‹―) + (Classical.choice β‹― - (↑(#Οƒ))⁻¹ β€’ Classical.choice β‹―)); k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) id⊒ (1 / ↑(#Οƒ)) β€’ βˆ‘ x ∈ Οƒ, x - (1 / ↑(#Οƒ)) β€’ (↑(#Οƒ) * Classical.choice β‹―) + Classical.choice β‹― = (1 / ↑(#Οƒ)) β€’ q + (((↑(#Οƒ) - 1) / (↑(#Οƒ) * (↑(#Οƒ) - 1))) β€’ βˆ‘ x ∈ Οƒ, x - ((↑(#Οƒ) - 1) / (↑(#Οƒ) * (↑(#Οƒ) - 1))) β€’ (↑(#Οƒ) * Classical.choice β‹―) - (((↑(#Οƒ) - 1) / (↑(#Οƒ) * (↑(#Οƒ) - 1))) β€’ q - ((↑(#Οƒ) - 1) / (↑(#Οƒ) * (↑(#Οƒ) - 1))) β€’ Classical.choice β‹―) + (Classical.choice β‹― - (1 / ↑(#Οƒ)) β€’ Classical.choice β‹―)); k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) id⊒ (1 / ↑(#Οƒ)) β€’ βˆ‘ x ∈ Οƒ, x - (1 / ↑(#Οƒ)) β€’ (↑(#Οƒ) * Classical.choice β‹―) + Classical.choice β‹― = (1 / ↑(#Οƒ)) β€’ q + ((1 / ↑(#Οƒ)) β€’ βˆ‘ x ∈ Οƒ, x - (1 / ↑(#Οƒ)) β€’ (↑(#Οƒ) * Classical.choice β‹―) - ((1 / ↑(#Οƒ)) β€’ q - (1 / ↑(#Οƒ)) β€’ Classical.choice β‹―) + (Classical.choice β‹― - (1 / ↑(#Οƒ)) β€’ Classical.choice β‹―)) ; All goals completed! πŸ™; have h_convex_comb : Finset.centroid ℝ Οƒ id ∈ openSegment ℝ q (Finset.centroid ℝ (Οƒ.erase q) id) := k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.val⊒ centroid ℝ Οƒ id βˆ‰ extremePoints ℝ P k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id ∈ openSegment ℝ q (centroid ℝ (Οƒ.erase q) id); k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ 0 < 1 / ↑(#Οƒ)k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ 0 < (↑(#Οƒ) - 1) / ↑(#Οƒ)k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ 1 / ↑(#Οƒ) + (↑(#Οƒ) - 1) / ↑(#Οƒ) = 1 ∧ (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ 0 < 1 / ↑(#Οƒ)k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ 0 < (↑(#Οƒ) - 1) / ↑(#Οƒ)k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ 1 / ↑(#Οƒ) + (↑(#Οƒ) - 1) / ↑(#Οƒ) = 1 ∧ (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ (↑(#Οƒ))⁻¹ + (↑(#Οƒ) - 1) / ↑(#Οƒ) = 1; k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ Οƒ.Nonempty All goals completed! πŸ™; k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ 0 < (↑(#Οƒ) - 1) / ↑(#Οƒ) All goals completed! πŸ™; k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ (↑(#Οƒ))⁻¹ + (↑(#Οƒ) - 1) / ↑(#Οƒ) = 1 k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ 1 + (↑(#Οƒ) - 1) = 1 * ↑(#Οƒ)k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ ↑(#Οƒ) β‰  0 k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ 1 + (↑(#Οƒ) - 1) = 1 * ↑(#Οƒ)k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) id⊒ ↑(#Οƒ) β‰  0 linarith [ show ( Οƒ.card : ℝ ) β‰₯ 2 k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.val⊒ centroid ℝ Οƒ id βˆ‰ extremePoints ℝ P All goals completed! πŸ™ ]; have h_convex_comb : q ∈ P ∧ Finset.centroid ℝ (Οƒ.erase q) id ∈ P := k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.val⊒ centroid ℝ Οƒ id βˆ‰ extremePoints ℝ P have h_convex_comb : Finset.centroid ℝ (Οƒ.erase q) id ∈ convexHull ℝ (Οƒ.erase q : Set (Fin k β†’ ℝ)) := k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.val⊒ centroid ℝ Οƒ id βˆ‰ extremePoints ℝ P k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb✝:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id ∈ openSegment ℝ q (centroid ℝ (Οƒ.erase q) id)⊒ IsStrictOrderedRing ℝk:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb✝:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id ∈ openSegment ℝ q (centroid ℝ (Οƒ.erase q) id)⊒ (Οƒ.erase q).Nonempty; k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb✝:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id ∈ openSegment ℝ q (centroid ℝ (Οƒ.erase q) id)⊒ IsStrictOrderedRing ℝ All goals completed! πŸ™; k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb✝:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id ∈ openSegment ℝ q (centroid ℝ (Οƒ.erase q) id)⊒ (Οƒ.erase q).Nonempty exact Finset.card_pos.mp ( k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb✝:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id ∈ openSegment ℝ q (centroid ℝ (Οƒ.erase q) id)⊒ 0 < #(Οƒ.erase q) k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb✝:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) idh_convex_comb:centroid ℝ Οƒ id ∈ openSegment ℝ q (centroid ℝ (Οƒ.erase q) id)⊒ 0 < #Οƒ - 1 ; All goals completed! πŸ™ ); All goals completed! πŸ™; k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valh:centroid ℝ Οƒ id ∈ extremePoints ℝ Pq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ q β‰  centroid ℝ (Οƒ.erase q) idh_convex_comb✝¹:centroid ℝ Οƒ id = (1 / ↑(#Οƒ)) β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) idh_convex_comb✝:centroid ℝ Οƒ id ∈ openSegment ℝ q (centroid ℝ (Οƒ.erase q) id)h_convex_comb:q ∈ P ∧ centroid ℝ (Οƒ.erase q) id ∈ Pthis:q = centroid ℝ Οƒ id⊒ False; k:β„•P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ PΟƒ:Finset (Fin k β†’ ℝ)hΟƒP:↑σ βŠ† Phcard:2 ≀ #Οƒhindep:AffineIndependent ℝ Subtype.valq:Fin k β†’ ℝhq:q ∈ Οƒ ∧ Β¬q = centroid ℝ (Οƒ.erase q) idh_convex_comb✝¹:q ∈ P ∧ centroid ℝ (Οƒ.erase q) id ∈ Ph:q ∈ extremePoints ℝ Ph_convex_comb✝:q = (↑(#Οƒ))⁻¹ β€’ q + ((↑(#Οƒ) - 1) / ↑(#Οƒ)) β€’ centroid ℝ (Οƒ.erase q) idh_convex_comb:q = centroid ℝ (Οƒ.erase q) idthis:True⊒ False; All goals completed! πŸ™ /- In a barycentric face, at most one vertex is an extreme point of `P`. -/ lemma baryFace_extreme_card_le_one (K : SimplicialComplex ℝ (Fin k β†’ ℝ)) {P : Set (Fin k β†’ ℝ)} (hPconv : Convex ℝ P) (hsub : βˆ€ Οƒ ∈ K.faces, (Οƒ : Set (Fin k β†’ ℝ)) βŠ† P) {s : Finset (Fin k β†’ ℝ)} (hs : s ∈ baryFaces K) : (s.filter (fun v => v ∈ Set.extremePoints ℝ P)).card ≀ 1 := k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Ps:Finset (Fin k β†’ ℝ)hs:s ∈ baryFaces K⊒ #({v ∈ s | v ∈ extremePoints ℝ P}) ≀ 1 k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonempty⊒ #({v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) ch | v ∈ extremePoints ℝ P}) ≀ 1; -- A vertex v ∈ s is the centroid of some Οƒ ∈ ch. By centroid_not_extreme_of_card_ge_two (with Οƒ βŠ† P from hsub since Οƒ ∈ K.faces, and Οƒ affinely independent from K.indep), if |Οƒ| β‰₯ 2 then centroid Οƒ is NOT an extreme point of P. have h_extreme_vertex : βˆ€ v ∈ ch.image (fun Οƒ => Finset.centroid ℝ Οƒ id), v ∈ Set.extremePoints ℝ P β†’ βˆƒ Οƒ ∈ ch, Οƒ.card = 1 ∧ v = Finset.centroid ℝ Οƒ id := k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Ps:Finset (Fin k β†’ ℝ)hs:s ∈ baryFaces K⊒ #({v ∈ s | v ∈ extremePoints ℝ P}) ≀ 1 intro v k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyv:Fin k β†’ ℝhv:v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) ch⊒ v ∈ extremePoints ℝ P β†’ βˆƒ Οƒ ∈ ch, #Οƒ = 1 ∧ v = centroid ℝ Οƒ id k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyv:Fin k β†’ ℝhv:v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) chhv_extreme:v ∈ extremePoints ℝ P⊒ βˆƒ Οƒ ∈ ch, #Οƒ = 1 ∧ v = centroid ℝ Οƒ id obtain βŸ¨Οƒ, hσ₁, hΟƒβ‚‚βŸ© : βˆƒ Οƒ ∈ ch, v = Finset.centroid ℝ Οƒ id := k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyv:Fin k β†’ ℝhv:v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) chhv_extreme:v ∈ extremePoints ℝ P⊒ βˆƒ Οƒ ∈ ch, v = centroid ℝ Οƒ id All goals completed! πŸ™; k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyv:Fin k β†’ ℝhv:v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) chhv_extreme:v ∈ extremePoints ℝ PΟƒ:Finset (Fin k β†’ ℝ)hσ₁:Οƒ ∈ chhΟƒβ‚‚:v = centroid ℝ Οƒ idhΟƒ_card:2 ≀ #ΟƒβŠ’ βˆƒ Οƒ ∈ ch, #Οƒ = 1 ∧ v = centroid ℝ Οƒ idk:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyv:Fin k β†’ ℝhv:v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) chhv_extreme:v ∈ extremePoints ℝ PΟƒ:Finset (Fin k β†’ ℝ)hσ₁:Οƒ ∈ chhΟƒβ‚‚:v = centroid ℝ Οƒ idhΟƒ_card:Β¬2 ≀ #ΟƒβŠ’ βˆƒ Οƒ ∈ ch, #Οƒ = 1 ∧ v = centroid ℝ Οƒ id; k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyv:Fin k β†’ ℝhv:v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) chhv_extreme:v ∈ extremePoints ℝ PΟƒ:Finset (Fin k β†’ ℝ)hσ₁:Οƒ ∈ chhΟƒβ‚‚:v = centroid ℝ Οƒ idhΟƒ_card:2 ≀ #ΟƒβŠ’ βˆƒ Οƒ ∈ ch, #Οƒ = 1 ∧ v = centroid ℝ Οƒ id exact False.elim <| hv_extreme.2 |> fun h => centroid_not_extreme_of_card_ge_two hPconv ( hsub Οƒ <| hch₁ hσ₁ ) hΟƒ_card ( K.indep <| hch₁ hσ₁ ) <| k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyv:Fin k β†’ ℝhv:v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) chhv_extreme:v ∈ extremePoints ℝ PΟƒ:Finset (Fin k β†’ ℝ)hσ₁:Οƒ ∈ chhΟƒβ‚‚:v = centroid ℝ Οƒ idhΟƒ_card:2 ≀ #Οƒh:βˆ€ ⦃x₁ : Fin k β†’ ℝ⦄, x₁ ∈ P β†’ βˆ€ ⦃xβ‚‚ : Fin k β†’ ℝ⦄, xβ‚‚ ∈ P β†’ v ∈ openSegment ℝ x₁ xβ‚‚ β†’ x₁ = v⊒ centroid ℝ Οƒ id ∈ extremePoints ℝ P All goals completed! πŸ™; k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyv:Fin k β†’ ℝhv:v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) chhv_extreme:v ∈ extremePoints ℝ PΟƒ:Finset (Fin k β†’ ℝ)hσ₁:Οƒ ∈ chhΟƒβ‚‚:v = centroid ℝ Οƒ idhΟƒ_card:Β¬2 ≀ #ΟƒβŠ’ βˆƒ Οƒ ∈ ch, #Οƒ = 1 ∧ v = centroid ℝ Οƒ id exact ⟨ Οƒ, hσ₁, le_antisymm ( not_lt.mp hΟƒ_card ) ( Finset.card_pos.mpr ( k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyv:Fin k β†’ ℝhv:v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) chhv_extreme:v ∈ extremePoints ℝ PΟƒ:Finset (Fin k β†’ ℝ)hσ₁:Οƒ ∈ chhΟƒβ‚‚:v = centroid ℝ Οƒ idhΟƒ_card:Β¬2 ≀ #ΟƒβŠ’ Οƒ.Nonempty k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyv:Fin k β†’ ℝhv:v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) chhv_extreme:v ∈ extremePoints ℝ PΟƒ:Finset (Fin k β†’ ℝ)hσ₁:Οƒ ∈ chhΟƒβ‚‚:v = centroid ℝ Οƒ idhΟƒ_card:Β¬2 ≀ #Οƒthis:Οƒ.Nonempty⊒ Οƒ.Nonempty ; All goals completed! πŸ™ ) ), hΟƒβ‚‚ ⟩; -- Since ch is a chain under βŠ†, it contains at most one singleton: two distinct singletons {a}, {b} are βŠ†-incomparable, contradicting IsChain. have h_singleton_chain : βˆ€ σ₁ Οƒβ‚‚, σ₁ ∈ ch β†’ Οƒβ‚‚ ∈ ch β†’ σ₁.card = 1 β†’ Οƒβ‚‚.card = 1 β†’ σ₁ = Οƒβ‚‚ := k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Ps:Finset (Fin k β†’ ℝ)hs:s ∈ baryFaces K⊒ #({v ∈ s | v ∈ extremePoints ℝ P}) ≀ 1 k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyh_extreme_vertex:βˆ€ v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) ch, v ∈ extremePoints ℝ P β†’ βˆƒ Οƒ ∈ ch, #Οƒ = 1 ∧ v = centroid ℝ Οƒ idσ₁:Finset (Fin k β†’ ℝ)Οƒβ‚‚:Finset (Fin k β†’ ℝ)hσ₁:σ₁ ∈ chhΟƒβ‚‚:Οƒβ‚‚ ∈ chhσ₁_card:#σ₁ = 1hΟƒβ‚‚_card:#Οƒβ‚‚ = 1⊒ σ₁ = Οƒβ‚‚ have h_singleton : βˆƒ a, σ₁ = {a} := k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Ps:Finset (Fin k β†’ ℝ)hs:s ∈ baryFaces K⊒ #({v ∈ s | v ∈ extremePoints ℝ P}) ≀ 1 All goals completed! πŸ™ have h_singleton' : βˆƒ b, Οƒβ‚‚ = {b} := k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Ps:Finset (Fin k β†’ ℝ)hs:s ∈ baryFaces K⊒ #({v ∈ s | v ∈ extremePoints ℝ P}) ≀ 1 All goals completed! πŸ™ k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyh_extreme_vertex:βˆ€ v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) ch, v ∈ extremePoints ℝ P β†’ βˆƒ Οƒ ∈ ch, #Οƒ = 1 ∧ v = centroid ℝ Οƒ idσ₁:Finset (Fin k β†’ ℝ)Οƒβ‚‚:Finset (Fin k β†’ ℝ)hσ₁:σ₁ ∈ chhΟƒβ‚‚:Οƒβ‚‚ ∈ chhσ₁_card:#σ₁ = 1hΟƒβ‚‚_card:#Οƒβ‚‚ = 1h_singleton':βˆƒ b, Οƒβ‚‚ = {b}a:Fin k β†’ ℝha:σ₁ = {a}⊒ σ₁ = Οƒβ‚‚ k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyh_extreme_vertex:βˆ€ v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) ch, v ∈ extremePoints ℝ P β†’ βˆƒ Οƒ ∈ ch, #Οƒ = 1 ∧ v = centroid ℝ Οƒ idσ₁:Finset (Fin k β†’ ℝ)Οƒβ‚‚:Finset (Fin k β†’ ℝ)hσ₁:σ₁ ∈ chhΟƒβ‚‚:Οƒβ‚‚ ∈ chhσ₁_card:#σ₁ = 1hΟƒβ‚‚_card:#Οƒβ‚‚ = 1a:Fin k β†’ ℝha:σ₁ = {a}b:Fin k β†’ ℝhb:Οƒβ‚‚ = {b}⊒ σ₁ = Οƒβ‚‚; k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyh_extreme_vertex:βˆ€ v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) ch, v ∈ extremePoints ℝ P β†’ βˆƒ Οƒ ∈ ch, #Οƒ = 1 ∧ v = centroid ℝ Οƒ idσ₁:Finset (Fin k β†’ ℝ)Οƒβ‚‚:Finset (Fin k β†’ ℝ)hσ₁:σ₁ ∈ chhΟƒβ‚‚:Οƒβ‚‚ ∈ chhσ₁_card:#σ₁ = 1hΟƒβ‚‚_card:#Οƒβ‚‚ = 1a:Fin k β†’ ℝha:σ₁ = {a}b:Fin k β†’ ℝhb:Οƒβ‚‚ = {b}h✝:σ₁ βŠ† Οƒβ‚‚βŠ’ σ₁ = Οƒβ‚‚k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyh_extreme_vertex:βˆ€ v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) ch, v ∈ extremePoints ℝ P β†’ βˆƒ Οƒ ∈ ch, #Οƒ = 1 ∧ v = centroid ℝ Οƒ idσ₁:Finset (Fin k β†’ ℝ)Οƒβ‚‚:Finset (Fin k β†’ ℝ)hσ₁:σ₁ ∈ chhΟƒβ‚‚:Οƒβ‚‚ ∈ chhσ₁_card:#σ₁ = 1hΟƒβ‚‚_card:#Οƒβ‚‚ = 1a:Fin k β†’ ℝha:σ₁ = {a}b:Fin k β†’ ℝhb:Οƒβ‚‚ = {b}h✝:Οƒβ‚‚ βŠ† Οƒβ‚βŠ’ σ₁ = Οƒβ‚‚ k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyh_extreme_vertex:βˆ€ v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) ch, v ∈ extremePoints ℝ P β†’ βˆƒ Οƒ ∈ ch, #Οƒ = 1 ∧ v = centroid ℝ Οƒ idσ₁:Finset (Fin k β†’ ℝ)Οƒβ‚‚:Finset (Fin k β†’ ℝ)hσ₁:σ₁ ∈ chhΟƒβ‚‚:Οƒβ‚‚ ∈ chhσ₁_card:#σ₁ = 1hΟƒβ‚‚_card:#Οƒβ‚‚ = 1a:Fin k β†’ ℝha:σ₁ = {a}b:Fin k β†’ ℝhb:Οƒβ‚‚ = {b}h✝:σ₁ βŠ† Οƒβ‚‚βŠ’ σ₁ = Οƒβ‚‚k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyh_extreme_vertex:βˆ€ v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) ch, v ∈ extremePoints ℝ P β†’ βˆƒ Οƒ ∈ ch, #Οƒ = 1 ∧ v = centroid ℝ Οƒ idσ₁:Finset (Fin k β†’ ℝ)Οƒβ‚‚:Finset (Fin k β†’ ℝ)hσ₁:σ₁ ∈ chhΟƒβ‚‚:Οƒβ‚‚ ∈ chhσ₁_card:#σ₁ = 1hΟƒβ‚‚_card:#Οƒβ‚‚ = 1a:Fin k β†’ ℝha:σ₁ = {a}b:Fin k β†’ ℝhb:Οƒβ‚‚ = {b}h✝:Οƒβ‚‚ βŠ† Οƒβ‚βŠ’ σ₁ = Οƒβ‚‚ All goals completed! πŸ™; k:β„•K:SimplicialComplex ℝ (Fin k β†’ ℝ)P:Set (Fin k β†’ ℝ)hPconv:Convex ℝ Phsub:βˆ€ Οƒ ∈ K.faces, ↑σ βŠ† Pch:Finset (Finset (Fin k β†’ ℝ))hch₁:↑ch βŠ† K.faceshchβ‚‚:IsChain (fun x1 x2 => x1 βŠ† x2) ↑chhch₃:ch.Nonemptyh_extreme_vertex:βˆ€ v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) ch, v ∈ extremePoints ℝ P β†’ βˆƒ Οƒ ∈ ch, #Οƒ = 1 ∧ v = centroid ℝ Οƒ idh_singleton_chain:βˆ€ (σ₁ Οƒβ‚‚ : Finset (Fin k β†’ ℝ)), σ₁ ∈ ch β†’ Οƒβ‚‚ ∈ ch β†’ #σ₁ = 1 β†’ #Οƒβ‚‚ = 1 β†’ σ₁ = Οƒβ‚‚βŠ’ βˆ€ a ∈ {v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) ch | v ∈ extremePoints ℝ P}, βˆ€ b ∈ {v ∈ Finset.image (fun Οƒ => centroid ℝ Οƒ id) ch | v ∈ extremePoints ℝ P}, a = b; All goals completed! πŸ™ end FamiliesOfMapsB01 end Submission

HelpersπŸ”—

Helpers.lean is an empty namespace, reserved by the project scaffolding:

namespace Submission.Helpers end Submission.Helpers