Commit 2023-01-27 06:03 7bdf589f

feat: port Topology.Bornology.Hom (#1855) porting notes:

1. In one place I had to provide explicitly the type of a hypothesis in a declaration which Lean 3 was able to infer from context.

• depends on: #1854