feat(topology/constructions): more convenient lemmas (#13423)
* Define `continuous.fst'` and friends and `continuous.compâ‚‚` and friends for convenience (and to help with elaborator issues)
* Cleanup in `topology/constructions`
* Define `set.preimage_inl_image_inr` and `set.preimage_inr_image_inl` and prove the `range` versions in terms of these. This required reordering some lemmas (moving general lemmas about `range` above the lemmas of interactions with `range` and specific functions).
* From the sphere eversion project
