{α : Type u_5} →
  {β : Type u_6} →
    [inst : PseudoMetricSpace α] →
      [inst_1 : PseudoMetricSpace β] →
        (f : α → β) → (∃ r, r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y) → α →ᵈ β