English
If d and d′ are ultrametrics on X taking values in a linearly ordered additive monoid, then their supremum metric d ⊔ d′ is ultrametric.
Русский
Если d и d′ — ультраметрические расстояния на X, принимающие значения в упорядоченном по сложности полугруппе, то их супремум d ⊔ d′ тоже ультраметрический.
LaTeX
$$$ (d \sqcup d')(x,z) \le \max\{(d \sqcup d')(x,y), (d \sqcup d')(y,z)\}. $$$
Lean4
instance sup [AddZeroClass R] [SemilatticeSup R] [AddLeftMono R] [AddRightMono R] {d d' : PseudoMetric X R} [IsUltra d]
[IsUltra d'] : IsUltra (d ⊔ d') := by
constructor
intro x y z
simp only [PseudoMetric.sup_apply]
calc
d x z ⊔ d' x z ≤ d x y ⊔ d y z ⊔ (d' x y ⊔ d' y z) := sup_le_sup le_sup le_sup
_ ≤ d x y ⊔ d' x y ⊔ (d y z ⊔ d' y z) := by simp [sup_comm, sup_left_comm]
