English
The Hamming distance satisfies the triangle inequality: d(x,z) ≤ d(x,y) + d(y,z).
Русский
Неравенство треугольника для расстояния Хэмминга: d(x,z) ≤ d(x,y) + d(y,z).
LaTeX
$$hammingDist(x,z) ≤ hammingDist(x,y) + hammingDist(y,z)$$
Lean4
/-- Corresponds to `dist_triangle`. -/
theorem hammingDist_triangle (x y z : ∀ i, β i) : hammingDist x z ≤ hammingDist x y + hammingDist y z := by
classical
unfold hammingDist
refine le_trans (card_mono ?_) (card_union_le _ _)
rw [← filter_or]
exact monotone_filter_right _ fun i h ↦ (h.ne_or_ne _).imp_right Ne.symm