Commit 2024-01-16 14:21 9ba98363

View on Github →

chore(Topology/Support): group related lemmas using a section (#9777) Only add a section; no lemmas are changed. Open the HasCompactSupport namespace more, while we're at it.

Estimated changes

Modified Mathlib/Topology/Support.lean

modified theorem HasCompactMulSupport.comp_closedEmbedding

modified theorem HasCompactMulSupport.comp_left

modified theorem HasCompactMulSupport.comp₂_left

modified theorem HasCompactMulSupport.intro'

modified theorem HasCompactMulSupport.intro

modified theorem HasCompactMulSupport.isCompact

modified theorem HasCompactMulSupport.isCompact_range

modified theorem HasCompactMulSupport.mono'

modified theorem HasCompactMulSupport.mono

modified theorem HasCompactMulSupport.of_mulSupport_subset_isCompact

modified theorem hasCompactMulSupport_comp_left

modified theorem hasCompactMulSupport_iff_eventuallyEq

modified theorem isCompact_range_of_mulSupport_subset_isCompact