Theorem EMetric.pair_reduction

Modification history

2026-08-13 16:41
Mathlib/Topology/EMetricSpace/PairReduction.lean
feat(Topology): generalize basic files to `Weak(Pseudo)EMetricSpace` (#42688) …
Modified EMetric.pair_reductionView on Github →
2025-10-16 08:57
Mathlib/Topology/EMetricSpace/PairReduction.lean
feat(Topology): Add PairReduction.lean (#26243) …
Added EMetric.pair_reductionView on Github →