English
There is a metric space structure on the product ∀n E_n with the distance defined by the first index where x and y differ.
Русский
Существует метрическая структура на произведении ∀n E_n, где расстояние задаётся по первому индексу, на котором x и y различаются.
LaTeX
$$$$ \operatorname{dist}(x,y)=\begin{cases}0, & x=y \\ (1/2)^{\operatorname{firstDiff}(x,y)}, & x\neq y\end{cases} $$$$
Lean4
/-- Metric space structure on `Π (n : ℕ), E n` when the spaces `E n` have the discrete topology,
where the distance is given by `dist x y = (1/2)^n`, where `n` is the smallest index where `x` and
`y` differ. Not registered as a global instance by default.
Warning: this definition makes sure that the topology is defeq to the original product topology,
but it does not take care of a possible uniformity. If the `E n` have a uniform structure, then
there will be two non-defeq uniform structures on `Π n, E n`, the product one and the one coming
from the metric structure. In this case, use `metricSpaceOfDiscreteUniformity` instead. -/
protected def metricSpace : MetricSpace (∀ n, E n) :=
MetricSpace.ofDistTopology dist PiNat.dist_self PiNat.dist_comm PiNat.dist_triangle isOpen_iff_dist
PiNat.eq_of_dist_eq_zero
