mathlib

44743821 - feat(category_theory/opposites): some opposite category properties (#2464)

feat(category_theory/opposites): some opposite category properties (#2464) Add some more basic properties relating to the opposite category. Make sure you have: * [x] reviewed and applied the coding style: [coding](https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/style.md), [naming](https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/naming.md) * [x] reviewed and applied [the documentation requirements](https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/doc.md) * [x] make sure definitions and lemmas are put in the right files * [x] make sure definitions and lemmas are not redundant For reviewers: [code review check list](https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/code-review.md) If you're confused by comments on your PR like `bors r+` or `bors d+`, please see our [notes on bors](https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/bors.md) for information on our merging workflow.