dist_prod_same_left — Mathlib

English

Keeping the left component fixed, the product metric reduces to the distance in the right component: dist((x,y1),(x,y2)) = dist(y1,y2).

Русский

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

LaTeX

$$$\operatorname{dist}((x,y_1),(x,y_2)) = \operatorname{dist}(y_1,y_2)$$$

Lean4

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

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