closedBall_prod_same — Mathlib

English

Similarly, closed balls multiply as: closedBall((x,y), r) = closedBall(x,r) × closedBall(y,r).

Русский

Замкнутые шары в произведении задаются аналогично: closedBall((x,y), r) = closedBall(x,r) × closedBall(y,r).

LaTeX

$$$\operatorname{closedBall}((x,y),r) = \operatorname{closedBall}(x,r) \\times \operatorname{closedBall}(y,r)$$$

Lean4

theorem closedBall_prod_same (x : α) (y : β) (r : ℝ) : closedBall x r ×ˢ closedBall y r = closedBall (x, y) r :=
  ext fun z => by simp [Prod.dist_eq]

Похожие утверждения