Theorem HasCompactMulSupport.of_mulSupport_subset_isCompact

Modification history

2025-08-03 18:11
Mathlib/Topology/Algebra/Support.lean
chore(Topology/Algebra/Support): misc. clean-ups; rename `HasCompactSupport.inv'` to `inv` (#27788) …
Modified HasCompactMulSupport.of_mulSupport_subset_isCompactView on Github →
2024-01-29 18:36
Mathlib/Topology/Support.lean
feat(Topology/Separation): define R₁ spaces, review API (#10085) …
Modified HasCompactMulSupport.of_mulSupport_subset_isCompactView on Github →
2024-01-29 06:37
Mathlib/Topology/Support.lean
feat: minor topological improvements (#9908) …
Modified HasCompactMulSupport.of_mulSupport_subset_isCompactView on Github →
2024-01-16 14:21
Mathlib/Topology/Support.lean
chore(Topology/Support): group related lemmas using a section (#9777) …
Modified HasCompactMulSupport.of_mulSupport_subset_isCompactView on Github →
2023-07-24 16:15
Mathlib/Topology/Support.lean
feat: Integrability of g • f for g continuous with compact support and f locally integrable (#6100)
Added HasCompactMulSupport.of_mulSupport_subset_isCompactView on Github →