[ooovi]

• porting convex joins to the new convexity following old convexity join
• using that to prove singleton is a face of the convex hull if it wasnt in the set in a cancellative convex space
• using that to prove krein milman without using homogenization following moritz' proof

depends on #119

[ooovi]

i'd be happy about some feedback to the convexCombPair_convexCombPair_convexCombPair_comm lemma which seems kind of terrible, but i fiddled with it a lot and this was the least annoying way to state it somehow. am i using the new convexity in a dumb way @YaelDillies ?

[YaelDillies]

Yes, there is a better way to state the comm lemma. The trick is to replace p, q by c * (p + q), d * (p + q) (so, if you are in a field, c = p / (p + q))

[YaelDillies]

Do we actually need this? I know I introduced the original mathlib definition, but I have doubted it ever since

[ooovi]

Yes, there is a better way to state the comm lemma. The trick is to replace p, q by c * (p + q), d * (p + q) (so, if you are in a field, c = p / (p + q))

I tried (see my most recent commit), but it's still pretty terrible. Maybe I misunderstood you.