closedBall_prod_same — Mathlib

English

In a pseudo-EMetric space, the product of radius-r closed balls equals the radius-r closed ball in the product space: closedBall(x, r) × closedBall(y, r) = closedBall((x, y), r).

Русский

В псевдоэмметрическом пространстве произведение закрытых шаров радиуса r равно закрытому шару в произведении пространств: closedBall(x, r) × closedBall(y, r) = closedBall((x, y), r).

LaTeX

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

Lean4

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

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