feat(topology/order): pasting lemmas

[ChrisHughes24]

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[rwbarton]

The two main gluing lemmas are pretty similar to continuous_subtype_nhds_cover and continuous_subtype_is_closed_cover. Does it make sense to merge these or at least reuse the proofs somehow?

[ChrisHughes24]

The two main gluing lemmas are pretty similar to continuous_subtype_nhds_cover and continuous_subtype_is_closed_cover. Does it make sense to merge these or at least reuse the proofs somehow?

I didn't realise there was any version of this lemma in mathlib. I don't have any particular reason to prefer my statement, I think the best thing is to close this PR, and just add some docstring on those lemmas containing gluing so people can find it more easily.

[rwbarton]

Ah, OK. Sounds good to me.