Commit 2020-07-21 12:58 49049e46
View on Github →feat(topology): implemented continuous bundled maps (#3486)
In this PR we defined continuous bundled maps, adapted the file compact_open accordingly, and proved instances of algebraic structures over the type continuous_map of continuous bundled maps. This feature was suggested on Zulip multiple times, see for example https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Continuous.20maps