fix: Rename theorems that use sorted instead of pairwise

[linesthatinterlace]

This PR renames theorems that use sorted in their name to instead use pairwise.

Closes #10742.

[linesthatinterlace]

awaiting-review

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-10-11 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-11 13:43:10)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase fb3e2c15fd8d50f5d97fcd1ea98899e83bdc3250 --onto efbbb0b230ce95653d25b59c83fd24a51a8bf363. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-23 12:33:44)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-11 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-10-11 13:43:12)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase fb3e2c15fd8d50f5d97fcd1ea98899e83bdc3250 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-23 12:33:45)

[TwoFX]

Could you add deprecations?

[linesthatinterlace]

@TwoFX I don't seem to be able to remove the "awaiting author" label but I have added the deprecations.

[TwoFX]

Thanks!