Commit 2025-02-21 13:27 f8a31488

View on Github →

chore: rename {Continuous., continuous_}sum_map to sumMap (#22155) To match the naming convention, successor of #22128.

Estimated changes

Modified Mathlib/Topology/Constructions.lean

added theorem Continuous.sumMap

deleted theorem Continuous.sum_map

added theorem continuous_sumMap

deleted theorem continuous_sum_map

Modified Mathlib/Topology/Homeomorph.lean