Commit 2024-07-22 07:17 18fafd29

View on Github →

feat(Topology/Algebra/PontryaginDual): Local Compactness of the Pontryagin Dual (#11335) This PR uses Arzela-Ascoli to prove local compactness of the Pontryagin dual.

Estimated changes

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

added theorem ContinuousMonoidHom.locallyCompactSpace_of_equicontinuousAt

added theorem ContinuousMonoidHom.locallyCompactSpace_of_hasBasis

Modified Mathlib/Topology/Algebra/PontryaginDual.lean