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)