dist of induced metric

Stream: Is there code for X?

[Winston Yin (尹維晨)]

How do I prove things about the dist induced by an injective map into a metric space? I can't seem to find a simple lemma relating the two metrics. Here's an mwe for my problem.

import Mathlib.Topology.ContinuousMap.Compact

structure MySpace (α β : Type*) [TopologicalSpace α] [CompactSpace α] [MetricSpace β] where
  toFun : α → β
  continuous : Continuous toFun

variable {α β : Type*} [TopologicalSpace α] [CompactSpace α] [MetricSpace β]

def MySpace.toContinuousMap : MySpace α β ↪ C(α, β) :=
  ⟨fun f ↦ ⟨f.toFun, f.continuous⟩, fun f β h ↦ by cases f; cases β; simpa using h⟩

noncomputable instance : MetricSpace (MySpace α β) :=
  MetricSpace.induced MySpace.toContinuousMap MySpace.toContinuousMap.injective inferInstance

example (f g : MySpace α β) (h : dist f.toContinuousMap g.toContinuousMap ≤ 3) :
    dist f g ≤ 3 := by
  have : dist f g = dist f.toContinuousMap g.toContinuousMap := rfl -- where's this lemma?
  rw [this]
  exact h

[Junyan Xu]

-- should be added to mathlib (for PseudoMetricSpace.Induced as well)
lemma isometry : Isometry (MySpace.toContinuousMap (α := α) (β := β)) :=
  fun _ _ ↦ rfl

example (f g : MySpace α β) (h : dist f.toContinuousMap g.toContinuousMap ≤ 3) :
    dist f g ≤ 3 := by
  rwa [← isometry.dist_eq]

[Winston Yin (尹維晨)]

Do you mean I should essentially add the lemma myself for every induced metric space I define? I would’ve expected this to come with induced.

[Etienne Marion]

I guess you want this:

import Mathlib.Topology.MetricSpace.Basic

variable {γ β : Type*} (f : γ → β) (hf : f.Injective) [m : MetricSpace β]

theorem dist_induced (x y : γ) : @dist γ (m.induced f hf).toDist x y = dist (f x) (f y) := rfl

I don't think it's in Mathlib

[Winston Yin (尹維晨)]

Thanks. I’ll PR this

[Junyan Xu]

I think these should be added:

import Mathlib.Topology.MetricSpace.Isometry

variable {α β : Type*}

lemma PseudoEMetricSpace.isometry_induced (f : α → β) (m : PseudoEMetricSpace β) :
    letI := m.induced f
    Isometry f :=
  fun _ _ ↦ rfl

lemma PsuedoMetricSpace.isometry_induced (f : α → β) (m : PseudoMetricSpace β) :
    letI := m.induced f
    Isometry f :=
  fun _ _ ↦ rfl

lemma EMetricSpace.isometry_induced (f : α → β) (hf : f.Injective) (m : EMetricSpace β) :
    letI := m.induced f hf
    Isometry f :=
  fun _ _ ↦ rfl

lemma MetricSpace.isometry_induced (f : α → β) (hf : f.Injective) (m : MetricSpace β) :
    letI := m.induced f hf
    Isometry f :=
  fun _ _ ↦ rfl

[Junyan Xu]

Note that there are already docs#IsUniformEmbedding.to_isometry and docs#Topology.IsEmbedding.to_isometry if you start from a uniform structure or a topology on α.

[Winston Yin (尹維晨)]

Thanks. I didn't think to check Isometry. I've submitted a PR at #20731