hammingDist_comm

Mathlib.InformationTheory.Hamming

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

English

Hamming distance is symmetric: d(x,y) = d(y,x).

Русский

Расстояние Хэмминга симметрично: d(x,y) = d(y,x).

LaTeX

$$hammingDist(x,y) = hammingDist(y,x)$$

Lean4

/-- Corresponds to `dist_comm`. -/
theorem hammingDist_comm (x y : ∀ i, β i) : hammingDist x y = hammingDist y x := by simp_rw [hammingDist, ne_comm]

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

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

Разделы

Аффилиация

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