hamming_zero_eq_dist

Mathlib.InformationTheory.Hamming

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

← MathLib Explorer

English

0 equals the distance if and only if x = y.

Русский

0 равно расстоянию тогда и только тогда, когда x = y.

LaTeX

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

Lean4

/-- Corresponds to `zero_eq_dist`. -/
@[simp]
theorem hamming_zero_eq_dist {x y : ∀ i, β i} : 0 = hammingDist x y ↔ x = y := by rw [eq_comm, hammingDist_eq_zero]

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

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

Разделы

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

Аффилиация

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