English
Let (i, x) and (j, y) be points in the disjoint union Σ_i E_i, where each E_i is a metric space with a chosen basepoint. The distance is defined by embedding each factor isometrically and using the basepoints: if i = j, the distance is the intrinsic distance in E_i; if i ≠ j, it is the sum of the distances from x and y to their respective basepoints plus 1 between the basepoints. This yields a distance on the disjoint union (depending on the choice of basepoints, hence not canonical).
Русский
Пусть (i, x) и (j, y) — точки в дизъюнктивном объединении Σ_i E_i, где каждый E_i — метрическое пространство с выбранной базовой точкой. Расстояние задаётся путем изометрического встраивания каждой пары; если i = j, расстояние равно внутреннему расстоянию в E_i; если i ≠ j, расстояние равно сумме расстояний от x и y до соответствующих базовых точек плюс 1 между базовыми точками. Это даёт расстояние на дизъюнктивном объединении (зависит от выбора базовых точек, следовательно не канонично).
LaTeX
$$$\displaystyle \mathrm{dist}((i,x),(j,y)) = \begin{cases} \mathrm{dist}_i(x,y), & i=j, \\[2pt] \mathrm{dist}_i(x,b_i) + 1 + \mathrm{dist}_j(b_j,y), & i\neq j, \end{cases}$ where $b_i \in E_i$ are fixed basepoints (one fixed choice for each $i$).$$
Lean4
/-- Distance on a disjoint union. There are many (noncanonical) ways to put a distance compatible
with each factor.
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 : (Σ i, E i) → (Σ i, E i) → ℝ
| ⟨i, x⟩, ⟨j, y⟩ =>
if h : i = j then
haveI : E j = E i := by rw [h]
Dist.dist x (cast this y)
else Dist.dist x (Nonempty.some ⟨x⟩) + 1 + Dist.dist (Nonempty.some ⟨y⟩) y
