Commit 2025-10-21 13:36 726f8bcd

View on Github →

chore(CompactlySupported): rename ContinuousMap.liftCompactlySupported (#30726)

Estimated changes

Modified Mathlib/Topology/ContinuousMap/CompactlySupported.lean

deleted def CompactlySupportedContinuousMap.ContinuousMap.liftCompactlySupported

added def CompactlySupportedContinuousMap.continuousMapEquiv