Commit 2025-01-14 12:01 b37ce20c

feat: isometries from induced metrics (#20731) If f : α → β, where β is a metric space, and the metric on α is induced by pullback along f, then f is an isometry. I add this trivial lemma for PseudoEmetricSpace, PseudoMetricSpace, EMetricSpace, and MetricSpace, as suggested by Junyan Xu in this thread.