Theorem PairReduction.iSup_edist_pairSet

Modification history

2026-08-13 16:41

Mathlib/Topology/EMetricSpace/PairReduction.lean

feat(Topology): generalize basic files to `Weak(Pseudo)EMetricSpace` (#42688) …

Modified PairReduction.iSup_edist_pairSet View on Github →

2025-10-16 08:57

Mathlib/Topology/EMetricSpace/PairReduction.lean

feat(Topology): Add PairReduction.lean (#26243) …

Added PairReduction.iSup_edist_pairSet View on Github →