mathlib

4e66c823 - feat(convex) continuity of real convex functions