Theorem Metric.mk_uniformity_basis_of_tendsto

Modification history

2026-06-14 04:43
Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
feat(Topology/Algebra/PontryaginDual): prove compact monoids have discrete duals (#38669) …
Added Metric.mk_uniformity_basis_of_tendstoView on Github →