Theorem EMetric.hausdorffEdist_singleton

Modification history

2025-11-03 03:00

Mathlib/Topology/MetricSpace/HausdorffDistance.lean

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

Added EMetric.hausdorffEdist_singleton View on Github →