nndist_eq_hammingDist — Mathlib

English

The nonnegative distance between two points x,y in Hamming β equals the Hamming distance between their images in the coordinate representation: nndist x y = hammingDist (ofHamming x) (ofHamming y).

Русский

Безотрицательное расстояние между x и y в Хэмминге β равно расстоянию Хэмминга между их образами: nndist x y = hammingDist(ofHamming x, ofHamming y).

LaTeX

$$$\\mathrm{nndist}(x,y) = hammingDist(\\operatorname{ofHamming}(x), \\operatorname{ofHamming}(y))$$$

Lean4

@[simp, push_cast]
theorem nndist_eq_hammingDist (x y : Hamming β) : nndist x y = hammingDist (ofHamming x) (ofHamming y) :=
  rfl

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