English
If β is nonempty, the closed/open ball in a product equals the product of the corresponding balls on each component.
Русский
Если β ненулево, то шар в произведении равен произведению шаров по компонентам.
LaTeX
$$$\mathrm{ball}(x,r) = \mathrm{Set.pi}\,\mathrm{univ}\, (\lambda b. \mathrm{ball}(x(b),r)).$$$
Lean4
/-- A sphere in a product space is a union of spheres on each component restricted to the closed
ball. -/
theorem sphere_pi (x : ∀ b, X b) {r : ℝ} (h : 0 < r ∨ Nonempty β) :
sphere x r = (⋃ i : β, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r :=
by
obtain hr | rfl | hr := lt_trichotomy r 0
· simp [hr]
· rw [closedBall_eq_sphere_of_nonpos le_rfl, eq_comm, Set.inter_eq_right]
letI := h.resolve_left (lt_irrefl _)
inhabit β
refine subset_iUnion_of_subset default ?_
intro x hx
replace hx := hx.le
rw [dist_pi_le_iff le_rfl] at hx
exact le_antisymm (hx default) dist_nonneg
· ext
simp [dist_pi_eq_iff hr, dist_pi_le_iff hr.le]
