Commit 2026-01-09 10:20 e55b59b1

View on Github ā†’

feat(ConvexSpace): complete proof_wanted statements (#33562) This PR proves the three proof_wanted statements for convexComboPair:

  • convexComboPair_zero: weight 0 on first point gives the second point
  • convexComboPair_one: weight 1 on first point gives the first point
  • convexComboPair_same: any convex combo of a point with itself is that point Also adds supporting lemmas:
  • StdSimplex.ext: extensionality lemma for StdSimplex
  • StdSimplex.mk_single: simp lemma for constructor applied to single
  • @[simp] attribute on ConvexSpace.single šŸ¤– Prepared with Claude Code

Estimated changes

added theorem StdSimplex.ext
added theorem StdSimplex.mk_single
added theorem convexComboPair_one
added theorem convexComboPair_same
added theorem convexComboPair_zero