dist_op — Mathlib

English

Distance is preserved by applying the operation op (multiplicative opposites) to both arguments: dist(op x, op y) = dist x y.

Русский

Расстояние сохраняется после применения операции op к обеим аргументах: dist(op x, op y) = dist x y.

LaTeX

$$$\\operatorname{dist}(\\operatorname{op} x, \\operatorname{op} y) = \\operatorname{dist}(x,y)$$$

Lean4

@[to_additive (attr := simp)]
theorem dist_op (x y : α) : dist (op x) (op y) = dist x y :=
  rfl

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