Modulus of convexity

Stream: maths

[Yaël Dillies]

Just for your information @Yury G. Kudryashov, I am defining the modulus and characteristic of convexity over at branch#convexity_modulus.

[Yury G. Kudryashov]

I left a few golfing suggestions at the top of https://github.com/leanprover-community/mathlib/commit/cc0467e8e83a8618bd3af3dd539bf8999c1e4fe4

[Yaël Dillies]

Oh thanks! I thought you might also have ideas about the new conditionally complete lemmas and whether I stated them correctly (for example, dropping dependence of f because of set.range).