Commit 2023-05-02 01:48 620ba06c

feat(analysis/convex/cone/proper): define closure of a convex cone (#16335) Part of #16266 We define the closure of a convex cone. This definition is only used for defining maps between proper cones and hence is in this file and not cone/basic.lean Next todo: define proper cones and add some proper cone API