Commit 2021-02-24 00:38 b4d2ce45

chore(data/equiv/local_equiv,topology/local_homeomorph,data/set/function): review (#6306)

data/equiv/local_equiv:

• move local_equiv.inj_on lemmas closer to each other, add missing lemmas;
• rename local_equiv.bij_on_source to local_equiv.bij_on;
• rename local_equiv.inv_image_target_eq_souce to local_equiv.symm_image_target_eq_souce;

data/set/function

• add set.inj_on.mem_of_mem_image, set.inj_on.mem_image_iff, set.inj_on.preimage_image_inter;
• add set.left_inv_on.image_image' and set.left_inv_on.image_image;
• add function.left_inverse.right_inv_on_range;
• move set.inj_on.inv_fun_on_image to golf the proof;

topology/local_homeomorph

• add lemmas like local_homeomorph.inj_on;
• golf the definition of open_embedding.to_local_homeomorph, make f explicit.