Commit 2025-11-03 03:00 3655c4d6

View on Github →

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

Estimated changes

Modified Mathlib/Topology/MetricSpace/Closeds.lean

added theorem EMetric.Closeds.isometry_singleton

added theorem EMetric.NonemptyCompacts.isometry_singleton

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean

added theorem EMetric.hausdorffEdist_singleton

added theorem Metric.hausdorffDist_singleton