feat(analysis/convex/cone): dual_of_dual_eq_self

[apurvnakade]

Proof that the dual of dual of a closed convex cone is itself. I'll break this result into smaller PRs. This result is fundamental to formalising linear (or rather conic) programming.

---

• [x] depends on #15639
• [x] depends on #15766

[apurvnakade]

~~TODO: I still need to add docstrings to these theorems and merge the previous branches.~~

[ocfnash]

Thanks! Please apply my suggestions and then feel free to merge.

bors d+

[bors[bot]]

:v: apurvnakade can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ocfnash]

Please also update the PR description: it seems to be out of date.

[apurvnakade]

Bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests