hammingDist_triangle_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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