English
Let X be a family of metric spaces indexed by a finite set β, and write Xb for the space at index b. For f,g: β → Xb, the distance between f and g in the product space (with the sup metric) equals the supremum over b of the distances between f(b) and g(b).
Русский
Пусть β — конечное множество индексов, и для каждого b ∈ β дано метрическое пространство X_b. Пусть f,g : β → X_b. Расстояние между f и g в произведении с верхним пределом равно наибольшему (_sup) расстоянию между компонентами: nndist(f,g)=sup_b nndist(f(b),g(b)).
LaTeX
$$$\mathrm{nndist}(f,g) = \sup_{b \in \mathrm{univ}} \mathrm{nndist}(f(b),g(b)).$$$
Lean4
theorem nndist_pi_def (f g : ∀ b, X b) : nndist f g = sup univ fun b => nndist (f b) (g b) :=
rfl
