English
The sphere in the product space decomposes as the union of two cylinder-like sets: sphere((x,y), r) = sphere(x,r) × closedBall(y,r) ∪ closedBall(x,r) × sphere(y,r).
Русский
Сфера в произведении разлагается на объединение двух цилиндрических множеств: sphere((x,y), r) = sphere(x,r) × closedBall(y,r) ∪ closedBall(x,r) × sphere(y,r).
LaTeX
$$$\operatorname{sphere}((x,y),r) = \operatorname{sphere}(x,r) \times \operatorname{closedBall}(y,r) \cup \operatorname{closedBall}(x,r) \times \operatorname{sphere}(y,r)$$$
Lean4
theorem sphere_prod (x : α × β) (r : ℝ) :
sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r :=
by
obtain hr | rfl | hr := lt_trichotomy r 0
· simp [hr]
· cases x
simp_rw [← closedBall_eq_sphere_of_nonpos le_rfl, union_self, closedBall_prod_same]
· ext ⟨x', y'⟩
simp_rw [Set.mem_union, Set.mem_prod, Metric.mem_closedBall, Metric.mem_sphere, Prod.dist_eq, max_eq_iff]
refine or_congr (and_congr_right ?_) (and_comm.trans (and_congr_left ?_))
all_goals rintro rfl; rfl
