Missing subspace lemma on balls

[CohenCyril]

Missing lemma from @ball subspace to the definition of subspace_ball

[affeldt-aist]

This lemma?

Section SubspacePseudoMetric.
Context {R : numDomainType} {X : pseudoMetricType R} (A : set X).

Lemma ball_subspace_ball (x : subspace A) r (y : subspace A) :
  ball x r y = subspace_ball x r y.
Proof. by []. Qed.

End SubspacePseudoMetric.