dist_prod_same_right — Mathlib

English

Keeping the right component fixed, the product metric reduces to the distance in the left component: dist((x1,y),(x2,y)) = dist(x1,x2).

Русский

При фиксированной правой компоненте произведение метрик сводится к расстоянию по левой компоненте: dist((x1,y),(x2,y)) = dist(x1,x2).

LaTeX

$$$\operatorname{dist}((x_1,y),(x_2,y)) = \operatorname{dist}(x_1,x_2)$$$

Lean4

@[simp]
theorem dist_prod_same_right {x₁ x₂ : α} {y : β} : dist (x₁, y) (x₂, y) = dist x₁ x₂ := by simp [Prod.dist_eq]

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