English
There is a Dist instance on the disjoint union Σ_i E_i defined by the rule above, i.e., a distance function on the disjoint union is given by the Sigma.dist construction.
Русский
Существует определение расстояния на дизъюнктивном объединении Σ_i E_i, заданное выше через конструкцию Sigma.dist.
LaTeX
$$$\text{dist}_{\Sigma} = \text{Sigma.dist}$$$
Lean4
/-- A `Dist` instance on the disjoint union `Σ i, E i`.
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. -/
def instDist : Dist (Σ i, E i) :=
⟨Sigma.dist⟩
