edist_le_pi_edist — Mathlib

English

For each index b, the distance between f(b) and g(b) is bounded above by the edist of the whole family.

Русский

Для каждого индекса b расстояние между f(b) и g(b) не превосходит edist всей семьи.

LaTeX

$$$\\operatorname{edist}(f(b), g(b)) \\le \\operatorname{edist} f g$$$

Lean4

theorem edist_le_pi_edist [∀ b, EDist (X b)] (f g : ∀ b, X b) (b : β) : edist (f b) (g b) ≤ edist f g :=
  le_sup (f := fun b => edist (f b) (g b)) (Finset.mem_univ b)

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