mathlib

bb01537b - feat(topology/local_homeomorph): a few facts about `local_homeomorph` (#2231)

feat(topology/local_homeomorph): a few facts about `local_homeomorph` (#2231) * `eventually_inv_right`, `eventually_inv_left` * `is_O_congr`, `is_o_congr` Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>