Commit 2025-06-02 08:55 9b46fb6e

View on Github →

feat: continuity of RestrictedProduct.map (#24915)

Estimated changes

Modified Mathlib/Topology/Algebra/RestrictedProduct.lean

added theorem RestrictedProduct.continuous_eval

added theorem RestrictedProduct.map_continuous