Ultrametric distances on pi types #
This file contains results on the behavior of ultrametrics in products of ultrametric spaces.
Main results #
Pi.instIsUltrametricDist: a product of ultrametric spaces is ultrametric.
ultrametric, nonarchimedean
instance
Pi.instIsUltrametricDist
{ι : Type u_1}
{X : ι → Type u_2}
[Fintype ι]
[(i : ι) → PseudoMetricSpace (X i)]
[∀ (i : ι), IsUltrametricDist (X i)]
:
IsUltrametricDist ((i : ι) → X i)