Theorem EMetric.NonemptyCompacts.isometry_singleton

Modification history

2025-11-03 03:00

Mathlib/Topology/MetricSpace/Closeds.lean

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

Added EMetric.NonemptyCompacts.isometry_singleton View on Github →