dist_pi_def — Mathlib

English

Let f,g: β → X_b with finite β. The distance between f and g in the product metric equals the real realization of the supremum of the componentwise NN-distances.

Русский

Пусть f,g : β → X_b, β конечное. Расстояние dist(f,g) в произведении равно реализацией числового супрема компонентных расстояний: dist(f,g)=(sup_{b} nndist(f(b),g(b))).toReal.

LaTeX

$$$\mathrm{dist}(f,g) = \left(\sup_{b \in \mathrm{univ}} \mathrm{nndist}(f(b),g(b))\right)^{\mathrm{toReal}}.$$$

Lean4

theorem dist_pi_def (f g : ∀ b, X b) : dist f g = (sup univ fun b => nndist (f b) (g b) : ℝ≥0) :=
  rfl

Похожие утверждения