Theorem Metric.ediam_pair

Modification history

2026-05-12 09:49

Mathlib/Topology/EMetricSpace/Diam.lean

feat: `min` and `max` theorems for `IsBotZeroClass` (#39057) …

Modified Metric.ediam_pair View on Github →

2026-01-06 17:14

Mathlib/Topology/EMetricSpace/Diam.lean

refactor(EMetricSpace): rename `EMetric.diam` -> `Metric.ediam` (#33558) …

Added Metric.ediam_pair View on Github →