mathlib

147b2943 - feat(analysis/convex/cone/proper): add hyperplane_separation and comap (#19008)

feat(analysis/convex/cone/proper): add hyperplane_separation and comap (#19008) We add the theorem `hyperplane_separation` which is a relative version of [convex_cone.hyperplane_separation_of_nonempty_of_is_closed_of_nmem](https://leanprover-community.github.io/mathlib_docs/analysis/convex/cone/dual.html#convex_cone.hyperplane_separation_of_nonempty_of_is_closed_of_nmem). This is the most general form of Farkas' lemma (that I know of) for convex cones. We also add `proper_cone.comap` and a few theorems about it. Co-authored-by: Apurva Nakade <apurvnakade@gmail.com@>