Theorem RestrictedProduct.mapAlong_continuous

Modification history

2025-07-31 19:52
Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.lean
feat: more RestrictedProduct API (#25715) …
Added RestrictedProduct.mapAlong_continuousView on Github →