hammingDist_triangle_right — Mathlib

English

A variant of the triangle inequality with the last argument fixed.

Русский

Вариант неравенства треугольника с фиксированным третьим аргументом.

LaTeX

$$hammingDist(x,y) ≤ hammingDist(x,z) + hammingDist(y,z)$$

Lean4

/-- Corresponds to `dist_triangle_right`. -/
theorem hammingDist_triangle_right (x y z : ∀ i, β i) : hammingDist x y ≤ hammingDist x z + hammingDist y z :=
  by
  rw [hammingDist_comm y]
  exact hammingDist_triangle _ _ _

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