English
For a countable family of metric spaces (F_i) indexed by i∈ι, one can define a product metric by dist(x,y) = sum' i min((1/2)^{encode i}, dist(x_i,y_i)).
Русский
Для счетного множества метрических пространств (F_i) индексируемых i ∈ ι можно ввести произведение-метрику: dist(x,y) = ∑' i min((1/2)^{encode i}, dist(x_i,y_i)).
LaTeX
$$$$\\\\operatorname{dist}:((i:ι)\\\\rightarrow F i) \\\\to \\\\mathbb{R}, \\\\n\\\\dist(x,y) = \\\\sum' i:ι, \\\\min((\\\\tfrac12)^{\\\\operatorname{encode} i},\\\\ dist(x_i,y_i)).$$$$
Lean4
/-- Given a countable family of metric spaces, one may put a distance on their product `Π i, E i`.
It is highly non-canonical, though, and therefore not registered as a global instance.
The distance we use here is `dist x y = ∑' i, min (1/2)^(encode i) (dist (x i) (y i))`. -/
protected def dist : Dist (∀ i, F i) :=
⟨fun x y => ∑' i : ι, min ((1 / 2) ^ encode i) (dist (x i) (y i))⟩
