Ultrametric distance on binary products

The product X × Y of two pseudometric spaces carries the sup distance dist x y = max (dist x.1 y.1) (dist x.2 y.2). When both factors are ultrametric, their binary product is again ultrametric, complementing Mathlib's Pi.instIsUltrametricDist for finite dependent products.

instance Prod.instIsUltrametricDist {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] [IsUltrametricDist X] [IsUltrametricDist Y] : IsUltrametricDist (X × Y)

The binary product of two ultrametric pseudometric spaces is ultrametric under the sup distance.