Formalizing subset of a metric space is a metric space

Stream: mathlib4

[The-Anh Vu-Le]

How do you formalize this result? "Let (X, d) be a metric space and A be a subset of X. Then, (A, dA) where dA = d on A x A is a metric space."

I can do

instance SubsetMetricSpace {X : Type*} (hX: MetricSpace X) (A : Set X) :
  MetricSpace A where
  eq_of_dist_eq_zero := by
    intro a₁ a₂ h
    exact MetricSpace.eq_of_dist_eq_zero h

but I was hoping for something having A ⊆ X instead of A : Set X (subset instead of subtype)

I hope this makes sense. If not, I will add more details about what I want to do.

[Ruben Van de Velde]

Not really, A : Set X is what I'd expect. Why don't you want that?

[Eric Wieser]

I think you're looking for docs#MetricSpace.induced