edist_pi_def — Mathlib

English

In the Pi-space setting, edistance between f and g is the supremum of component edistances.

Русский

В отношении Π-пространства edist(f,g) — супремум компонентных edist.

LaTeX

$$$\\operatorname{edist}(f,g) = \\operatorname{Finset}.sup_{b\\in \\mathrm{univ}} \\operatorname{edist}(f(b), g(b))$$$

Lean4

theorem edist_pi_def [∀ b, EDist (X b)] (f g : ∀ b, X b) : edist f g = Finset.sup univ fun b => edist (f b) (g b) :=
  rfl

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