hammingDist_triangle — Mathlib

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

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