mathlib

620ba06c - feat(analysis/convex/cone/proper): define closure of a convex cone (#16335)

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 Co-authored-by: Apurva Nakade <apurvnakade@gmail.com@>