hammingDist_eq_zero

Mathlib.InformationTheory.Hamming

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

← MathLib Explorer

English

The zero-distance equivalence characterizes equality of functions.

Русский

Искомое равенство нулю расстояния эквивалентно равенству функций.

LaTeX

$$hammingDist(x,y) = 0 \iff x = y$$

Lean4

/-- Corresponds to `dist_eq_zero`. -/
@[simp]
theorem hammingDist_eq_zero {x y : ∀ i, β i} : hammingDist x y = 0 ↔ x = y :=
  ⟨eq_of_hammingDist_eq_zero, fun H => by
    rw [H]
    exact hammingDist_self _⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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