Distance from point in metric space to subset

Stream: Is there code for X?

[Samuel Webb]

Screenshot-2023-11-06-at-12.49.44.png

Let $(X, d)$ be a metric space, let $x \in X, y \in X$ and $A \subset X$, with $A$ non-empty. Then $|d(x, A) - d(y, A)| \leq d(x,y)$

Currently trying to construct a proof for this theorem but I am struggling to find anything regarding distance from points in a metric space to subset of said metric space. Any help would be very much appreciated. My apologies if this is the wrong place for this question.

[Eric Wieser]

Have you managed to construct a statement of this theorem? If so, you'd be able to ask it as a #mwe, and might get help faster :)

[Samuel Webb]

Sorry I wasn't clear. I haven't managed to construct a statement of the theorem. This is really what I am looking for help with.

[Ruben Van de Velde]

What is your definition of $d(x, A)$?

[Samuel Webb]

$d(x, A) := inf\{d(x,y) : y \in A\}$

[Eric Wieser]

Perhaps docs#Metric.infDist ?

[Samuel Webb]

That looks very helpful I will check that out. Thank you.

[Ruben Van de Velde]

Thanks, Ericsearch :)

[Kevin Buzzard]

If you need any further help then by far the best way to ask for it here is to post fully working Lean code rather than LaTeX. See the #mwe link.

[Samuel Webb]

Thank you I will try to when I have any working code for this theorem.