关于度量空间紧子集距离上确界可达性证明的特定解法咨询

嘿，我对实分析里这个关于紧性的问题的某类解法有一些疑问~

得先说明下，这个问题和“证明$\mathbb{R}^2$中紧集能达到上确界”的问题不是一回事，因为我关注的是另一种完全不同的解法思路。

问题陈述 #

设$(X, \partial)$是一个度量空间，$K$是$X$的一个紧子集。请证明：存在$x_0, y_0 \in K$，使得
$$
\partial(x_0, y_0) = \sup {\partial(x, y) \mid x, y \in K}
$$

解法片段 #

• 第一步：定义函数
  对任意固定的$x \in K$，定义函数$f_x : K \to \mathbb{R}$，满足：
  $$
  f_x(y) = \partial(x, y)
  $$
  （注：原解法内容在这里截断了，后续步骤未完整给出）

备注：内容来源于stack exchange，提问作者Aleem