hammingDist_pos

Mathlib.InformationTheory.Hamming

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

← MathLib Explorer

English

The distance is positive exactly when the two inputs are different.

Русский

Расстояние положительно тогда, когда входы различны.

LaTeX

$$0 < hammingDist(x,y) \iff x ≠ y$$

Lean4

/-- Corresponds to `dist_pos`. -/
@[simp]
theorem hammingDist_pos {x y : ∀ i, β i} : 0 < hammingDist x y ↔ x ≠ y := by
  rw [← hammingDist_ne_zero, iff_not_comm, not_lt, Nat.le_zero]

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

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

Разделы

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

Аффилиация

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