mathlib

f7313156 - feat(topology/local_homeomorph): "injectivity" local_homeomorph.prod (#15311)

feat(topology/local_homeomorph): "injectivity" local_homeomorph.prod (#15311) * Also some other lemmas about `local_equiv` and `local_homeomorph` * From the sphere eversion project