hammingDist

Mathlib.InformationTheory.Hamming

URI: https://scilib.ai/kg/mathlib#hammingDist

English

The Hamming distance between two families of elements is always a nonnegative integer.

Русский

Расстояние Хэмминга между двумя семействами признаков всегда неотрицательно и натурально.

LaTeX

$$0 \le hammingDist(x,y)$$

Lean4

/-- The Hamming distance function to the naturals. -/
def hammingDist (x y : ∀ i, β i) : ℕ :=
  #{i | x i ≠ y i}

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru