English
For f,g: β → X_b and r>0, dist(f,g) = r iff there exists i with dist(f(i),g(i)) = r and ∀ b, dist(f(b),g(b)) ≤ r.
Русский
Для f,g: β → X_b и r>0: dist(f,g)=r тогда и только тогда, когда существует i с dist(f(i),g(i))=r и для всех b выполняется dist(f(b),g(b)) ≤ r.
LaTeX
$$$\mathrm{dist}(f,g) = r \iff (\exists i, \mathrm{dist}(f(i),g(i)) = r) \land \forall b, \mathrm{dist}(f(b),g(b)) \le r.$$$
Lean4
/-- A closed ball in a product space is a product of closed balls. See also `closedBall_pi'`
for a version assuming `Nonempty β` instead of `0 ≤ r`. -/
theorem closedBall_pi (x : ∀ b, X b) {r : ℝ} (hr : 0 ≤ r) : closedBall x r = Set.pi univ fun b => closedBall (x b) r :=
by
ext p
simp [dist_pi_le_iff hr]
