English
Let (X_b)_{b∈β} be a finite family of spaces with an edistance edist. For f,g : ∀ b, X_b and d ∈ ℝ≥0∞, we have edist f g ≤ d if and only if for every b ∈ β, edist (f b) (g b) ≤ d.
Русский
Пусть (X_b)_(b∈β) является конечной совокупностью пространств с расстоянием edist. Для функций f,g : ∀ b, X_b и числа d ∈ ℝ≥0∞ верно: edist f g ≤ d тогда и только если для каждого b ∈ β выполняется edist (f b) (g b) ≤ d.
LaTeX
$$$$ edist f g \\le d \\iff \\forall b, edist (f b) (g b) \\le d. $$$$
Lean4
theorem edist_pi_le_iff [∀ b, EDist (X b)] {f g : ∀ b, X b} {d : ℝ≥0∞} : edist f g ≤ d ↔ ∀ b, edist (f b) (g b) ≤ d :=
Finset.sup_le_iff.trans <| by simp only [Finset.mem_univ, forall_const]
