isometry induced

Mathlib/Topology/MetricSpace/Isometry.lean

@@ -258,6 +258,18 @@ theorem Topology.IsEmbedding.to_isometry {α β} [TopologicalSpace α] [MetricSp
 @[deprecated (since := "2024-10-26")]
 alias Embedding.to_isometry := IsEmbedding.to_isometry
 
+theorem PseudoEMetricSpace.isometry_induced (f : α → β) [m : PseudoEMetricSpace β] :
+    letI := m.induced f; Isometry f := fun _ _ ↦ rfl
+
+theorem PsuedoMetricSpace.isometry_induced (f : α → β) [m : PseudoMetricSpace β] :
+    letI := m.induced f; Isometry f := fun _ _ ↦ rfl
+
+theorem EMetricSpace.isometry_induced (f : α → β) (hf : f.Injective) [m : EMetricSpace β] :
+    letI := m.induced f hf; Isometry f := fun _ _ ↦ rfl
+
+theorem MetricSpace.isometry_induced (f : α → β) (hf : f.Injective) [m : MetricSpace β] :
+    letI := m.induced f hf; Isometry f := fun _ _ ↦ rfl
+
 -- such a bijection need not exist
 /-- `α` and `β` are isometric if there is an isometric bijection between them. -/
 -- Porting note (https://github.com/leanprover-community/mathlib4/issues/5171): was @[nolint has_nonempty_instance]