Commit 2023-12-19 16:45 9bf055e5

refactor(Topology/IsLocalHomeomorph): various small clean-ups (#9150)

• revamp and extend the module docstring
• add some lemma docstrings
• use EqOn where possible
• use \mapsto instead of =>
• replace one terminal rfl by the explicit lemma invoked