Category of metric spaces and isometries

The category $𝖨 𝗌 𝗈 𝖬 𝖾 𝗍$ contains metric spaces as its objects and isometries as its morphisms, #m/def/anal i.e. if $(𝑋, 𝑑 𝑋)$ and $(𝑌, 𝑑 𝑌)$ are metric spaces, a morphism $𝑓 \in 𝖨 𝗌 𝗈 𝖬 𝖾 𝗍 ((𝑋, 𝑑 𝑋), (𝑌, 𝑑 𝑌))$ is a function $𝑓 : 𝑋 \to 𝑌$ such that

𝑑 𝑋 (𝑎, 𝑏) = 𝑑 𝑌 (𝑓 (𝑎), 𝑓 (𝑏))

for any $𝑎, 𝑏 \in 𝑋$ .

#state/tidy | #lang/en | #SemBr