hammingDist_lt_one

Mathlib.InformationTheory.Hamming

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

English

The distance is less than 1 exactly when the inputs are equal.

Русский

Расстояние меньше единицы тогда и только тогда, когда входы равны.

LaTeX

$$hammingDist(x,y) < 1 \iff x = y$$

Lean4

theorem hammingDist_lt_one {x y : ∀ i, β i} : hammingDist x y < 1 ↔ x = y := by rw [Nat.lt_one_iff, hammingDist_eq_zero]

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

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

Разделы

Аффилиация

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