English
A sphere in a product space is the union of componentwise spheres intersected with the product ball.
Русский
Сфера в произведении является объединением сфер по компонентам, ограниченных шаром в произведении.
LaTeX
$$$\mathrm{sphere}(x,r) = \bigcup_{i\in \beta} \mathrm{preimage}(\mathrm{eval}\,i)(\mathrm{sphere}(x_i,r)) \cap \mathrm{closedBall}(x,r).$$$
Lean4
/-- A closed ball in a product space is a product of closed balls. See also `closedBall_pi`
for a version assuming `0 ≤ r` instead of `Nonempty β`. -/
theorem closedBall_pi' [Nonempty β] (x : ∀ b, X b) (r : ℝ) : closedBall x r = Set.pi univ fun b => closedBall (x b) r :=
(le_or_gt 0 r).elim (closedBall_pi x) fun hr => by simp [closedBall_eq_empty.2 hr]
