Theorem Metric.isBounded_iff_ediam_ne_top

Modification history

2026-01-06 17:14
Mathlib/Topology/MetricSpace/Bounded.lean
refactor(EMetricSpace): rename `EMetric.diam` -> `Metric.ediam` (#33558) …
Modified Metric.isBounded_iff_ediam_ne_topView on Github →
2023-10-30 10:24
Mathlib/Topology/MetricSpace/Basic.lean
chore: split MetricSpace.basic (#7920) …
Modified Metric.isBounded_iff_ediam_ne_topView on Github →
2023-09-19 04:03
Mathlib/Topology/MetricSpace/Basic.lean
refactor(Topology/MetricSpace): remove `Metric.Bounded` (#7240) …
Added Metric.isBounded_iff_ediam_ne_topView on Github →