English
For f,g: β → X_b and any r, dist f g = r is equivalent to the existence of i with dist(f(i),g(i)) = r and all components are ≤ r in distance.
Русский
Для функций f,g: β → X_b и произвольного r, dist(f,g)=r эквивалентно существованию i с dist(f(i),g(i))=r и для всех компонент dist(f(b),g(b)) ≤ r.
LaTeX
$$$\mathrm{dist}(f,g) = r \iff \big(\exists i, (\mathrm{dist}(f(i),g(i)) = r)\big) \land \forall b, \mathrm{dist}(f(b),g(b)) \le r.$$$
Lean4
theorem dist_pi_le_iff' [Nonempty β] {f g : ∀ b, X b} {r : ℝ} : dist f g ≤ r ↔ ∀ b, dist (f b) (g b) ≤ r :=
by
by_cases hr : 0 ≤ r
· exact dist_pi_le_iff hr
·
exact
iff_of_false (fun h => hr <| dist_nonneg.trans h) fun h => hr <| dist_nonneg.trans <| h <| Classical.arbitrary _
