English
There is a metric space structure on the disjoint union Σ_i E_i defined by the Sigma-based distance.
Русский
На дизъюнктивном объединении Σ_i E_i задана структура метрического пространства с помощью расстояния Sigma.
LaTeX
$$$\text{There exists a metric space structure on }\Sigma_i E_i\text{ with distance } \mathrm{dist}_{\Sigma}. $$$
Lean4
/-- A metric space structure 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. -/
protected def metricSpace : MetricSpace (Σ i, E i) :=
by
refine MetricSpace.ofDistTopology Sigma.dist ?_ ?_ Sigma.dist_triangle Sigma.isOpen_iff ?_
· rintro ⟨i, x⟩
simp [Sigma.dist]
· rintro ⟨i, x⟩ ⟨j, y⟩
rcases eq_or_ne i j with (rfl | h)
· simp [Sigma.dist, dist_comm]
· simp only [Sigma.dist, dist_comm, h, h.symm, not_false_iff, dif_neg]
abel
· rintro ⟨i, x⟩ ⟨j, y⟩
rcases eq_or_ne i j with (rfl | hij)
· simp [Sigma.dist]
· intro h
apply (lt_irrefl (1 : ℝ) _).elim
calc
1 ≤ Sigma.dist (⟨i, x⟩ : Σ k, E k) ⟨j, y⟩ := Sigma.one_le_dist_of_ne hij _ _
_ < 1 := by rw [h]; exact zero_lt_one
