Theorem Metric.hausdorffDist_singleton

Modification history

2025-11-03 03:00

Mathlib/Topology/MetricSpace/HausdorffDistance.lean

feat(Topology/MetricSpace): Hausdorff distance of singleton sets (#31060)

Added Metric.hausdorffDist_singleton View on Github →