ball_prod_same — Mathlib

English

In the max metric, the product of balls equals the ball in the product space: ball((x,y), r) = ball(x,r) × ball(y,r).

Русский

В максимальной метрике произведение шаров эквивалентно шару в произведении: ball((x,y), r) = ball(x,r) × ball(y,r).

LaTeX

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

Lean4

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

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