Theorem RestrictedProduct.map_continuous

Modification history

2025-07-31 19:52
Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.lean
feat: more RestrictedProduct API (#25715) …
Deleted RestrictedProduct.map_continuousView on Github →
2025-06-02 08:55
Mathlib/Topology/Algebra/RestrictedProduct.lean
feat: continuity of RestrictedProduct.map (#24915)
Added RestrictedProduct.map_continuousView on Github →