Commit 2025-12-08 03:56 5e943c75
View on Github →feat: convex combinations in Set.Icc (#31525)
This will hopefully become obsolete with a more general theory of convex spaces, but this would be helpful to go on for now.
Note: Proofs in this PR were developed with assistance from Claude.