Continuity of Distance and Norm (距離関数・ノルムの連続性) (Example IV.2.4)

• Continuity of Distance and Norm (距離関数・ノルムの連続性) (Example IV.2.4) #Card
  • 距離化可能な $\xi$ と両立距離 $d$ について $d(\cdot, x)$ はどんな写像か。

Back

If $d$ is a metric compatible with a metrizable convergence $\xi$ on $X$, then $d(\cdot, x) \in C(\xi, \nu_\mathbb{R})$ for each $x \in X$.

鍵は逆三角不等式: 三角不等式と対称性から $$|d(y, x) - d(z, x)| \leq d(y, z),$$ これと Example IV.2.3（$\varepsilon$–$\delta$）で連続性が出る。$X$ がノルム空間なら $|x| = d(x, 0)$ よりノルムは連続。

Lean

continuous_dist / Continuous.dist / continuous_norm