mathlib

42d64072 - feat(analysis/convex/cone): add `inner_dual_cone_of_inner_dual_cone_eq_self` for nonempty, closed, convex cones (#15637)

feat(analysis/convex/cone): add `inner_dual_cone_of_inner_dual_cone_eq_self` for nonempty, closed, convex cones (#15637) We add the following results about convex cones: - instance `has_zero` - `inner_dual_cone_zero` - `inner_dual_cone_univ` - `pointed_of_nonempty_of_is_closed` - `hyperplane_separation_of_nonempty_of_is_closed_of_nmem` - `inner_dual_cone_of_inner_dual_cone_eq_self` References: - https://ti.inf.ethz.ch/ew/lehre/ApproxSDP09/notes/conelp.pdf - Stephen P. Boyd and Lieven Vandenberghe. Convex Optimization. Cambridge University Press. ISBN 978-0-521-83378-3. available at https://web.stanford.edu/~boyd/cvxbook/bv_cvxbook.pdf