nndist_toDual — Mathlib

English

The distance between a and b is preserved under the dual construction: nndist(toDual a, toDual b) = nndist(a, b).

Русский

Расстояние между элементами сохраняется при переходе к двойственному порядку: nndist(toDual a, toDual b) = nndist a b.

LaTeX

$$$\mathrm{nndist}(\mathrm{toDual}(a),\mathrm{toDual}(b)) = \mathrm{nndist}(a,b)$$$

Lean4

@[simp]
theorem nndist_toDual (a b : X) : nndist (toDual a) (toDual b) = nndist a b :=
  rfl

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