English
If each X_i is an ultrametric space and ι is finite, then the product space ∏_{i∈ι} X_i with the sup metric is ultrametric.
Русский
Если для конечного множества индексов i ∈ ι каждая X_i — ультраметрическое пространство, то произведение с помощью максимального (суп) расстояния является ультраметрическим пространством.
LaTeX
$$IsUltrametricDist (∏_{i∈ι} X_i)$$
Lean4
instance instIsUltrametricDist {ι : Type*} {X : ι → Type*} [Fintype ι] [(i : ι) → PseudoMetricSpace (X i)]
[(i : ι) → IsUltrametricDist (X i)] : IsUltrametricDist ((i : ι) → X i) :=
by
constructor
intro f g h
simp only [dist_pi_def, ← NNReal.coe_max, NNReal.coe_le_coe, ← Finset.sup_sup]
exact Finset.sup_mono_fun fun i _ ↦ IsUltrametricDist.dist_triangle_max (f i) (g i) (h i)
