English
Finite sup of ultrametrics remains ultrametric: the supremum over a finite index set of ultrametric distances is ultrametric.
Русский
Конечный супремум ультраметрических расстояний сохраняет ультраметричность: сумма по конечному индексу ультраметрических расстояний также ультраметрическая.
LaTeX
$$$ (s \sup f)(x,z) \le \max\{(s \sup f)(x,y), (s \sup f)(y,z)\}. $$$
Lean4
theorem finsetSup {Y : Type*} [AddCommMonoid R] [LinearOrder R] [AddLeftStrictMono R] [IsOrderedAddMonoid R]
{f : Y → PseudoMetric X R} {s : Finset Y} (h : ∀ d ∈ s, IsUltra (f d)) : IsUltra (s.sup f) :=
by
constructor
intro x y z
rcases s.eq_empty_or_nonempty with rfl | hs
· simp
simp_rw [finsetSup_apply hs]
apply Finset.sup'_le
simp only [le_sup_iff, Finset.le_sup'_iff]
intro i hi
have h := (h i hi).le_sup' x y z
simp only [le_sup_iff] at h
refine h.imp ?_ ?_ <;> intro H <;> exact ⟨i, hi, H⟩
