Commit 2022-04-21 23:36 1e76b9eb

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