Theorem EMetric.diam_pi_le_of_le
Modification history
2025-07-11 18:12
Mathlib/Topology/EMetricSpace/Diam.lean
chore(Topology): rename pi family from π to X (#26828) …
Modified EMetric.diam_pi_le_of_leView on Github →2024-08-16 01:08
Mathlib/Topology/EMetricSpace/Basic.lean
chore: splitting up metric spaces files (#15790)
Modified EMetric.diam_pi_le_of_leView on Github →