Commit 2022-08-04 08:27 4f3245c3
View on Github →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