mathlib3

bec8b65e - feat(analysis/calculus/tangent_cone): unique differentiability of open interval at endpoint (#14530)

feat(analysis/calculus/tangent_cone): unique differentiability of open interval at endpoint (#14530) We show that, if a point belongs to the closure of a convex set with nonempty interior, then it is a point of unique differentiability. We apply this to the specific situation of `Ioi` and `Iio`.