English
The left and right injections into a disjoint union are isometries with respect to Sum.dist, hence the sum distance extends the original component distances.
Русский
Левые и правые вложения в дискретное объединение являются изометриями относительно Sum.dist, следовательно, сумма-дистанция расширяет дистанции компонент.
LaTeX
$$$ \mathrm{isometry\_inl} :\; \mathrm{Isometry}(\mathrm{Sum.inl}) ,\quad \mathrm{isometry\_inr} :\; \mathrm{Isometry}(\mathrm{Sum.inr}). $$$
Lean4
/-- Distance on a disjoint union. There are many (noncanonical) ways to put a distance compatible
with each factor.
If the two spaces are bounded, one can say for instance that each point in the first is at distance
`diam X + diam Y + 1` of each point in the second.
Instead, we choose a construction that works for unbounded spaces, but requires basepoints,
chosen arbitrarily.
We embed isometrically each factor, set the basepoints at distance 1,
arbitrarily, and say that the distance from `a` to `b` is the sum of the distances of `a` and `b` to
their respective basepoints, plus the distance 1 between the basepoints.
Since there is an arbitrary choice in this construction, it is not an instance by default. -/
protected def dist : X ⊕ Y → X ⊕ Y → ℝ
| .inl a, .inl a' => dist a a'
| .inr b, .inr b' => dist b b'
| .inl a, .inr b => dist a (Nonempty.some ⟨a⟩) + 1 + dist (Nonempty.some ⟨b⟩) b
| .inr b, .inl a => dist b (Nonempty.some ⟨b⟩) + 1 + dist (Nonempty.some ⟨a⟩) a
