mathlib3

4f3245c3 - feat(topology/continuous_function/basic): inverse equations for `homeomorph.to_continuous_map` (#15708)

feat(topology/continuous_function/basic): inverse equations for `homeomorph.to_continuous_map` (#15708) This PR adds two lemmas stating the left and right inverse of an `homeomorph.to_continuous_map`: -`homeomorph.symm_comp_to_continuous_map`, and -`homeomorph.comp_symm_to_continuous_map` Suggested by: @alreadydone Co-authored-by: Junyan Xu <junyanxumath@gmail.com>