Commit 2025-08-03 18:11 c484c5fe

View on Github →

chore(Topology/Algebra/Support): misc. clean-ups; rename HasCompactSupport.inv' to inv (#27788) Companion to #27777.

Estimated changes

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Topology/Algebra/Support.lean

modified theorem HasCompactMulSupport.intro'

modified theorem HasCompactMulSupport.intro

modified theorem HasCompactMulSupport.isCompact

modified theorem HasCompactMulSupport.isCompact_preimage

modified theorem HasCompactMulSupport.mono'

modified theorem HasCompactMulSupport.mono

modified theorem HasCompactMulSupport.of_mulSupport_subset_isCompact

Modified Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean