dist_eq_hammingDist — Mathlib

English

For x,y ∈ Hamming β, the metric distance dist x y equals the Hamming distance between their representations as functions on β.

Русский

Для любых x,y ∈ Hamming β расстояние dist x y равно расстоянию Хэмминга между их образами как функций на β.

LaTeX

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

Lean4

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

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