ball_prod_same — Mathlib

English

Let α and β be spaces with a pseudo-EMetric. For any x in α, y in β and radius r, the product of the radius-r balls equals the radius-r ball in the product space: ball(x, r) × ball(y, r) = ball((x, y), r).

Русский

Пусть α и β — пространства с псевдоэмметрикой. Для любых x ∈ α, y ∈ β и радиуса r произведение шаров радиуса r равно шарeм в произведении пространств: ball(x, r) × ball(y, r) = ball((x, y), r).

LaTeX

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

Lean4

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

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