hammingDist_smul_le_hammingDist — Mathlib

English

If each coordinate is smul-compatible, then scaling both inputs by a common scalar does not increase the Hamming distance.

Русский

Если каждое координатное пространство совместимо со скаляром, масштабирование обеих функций тем же скаляром не увеличивает расстояние Хэмминга.

LaTeX

$$hammingDist( (k • x_i) , (k • y_i) ) ≤ hammingDist( x_i , y_i ) for all i$$

Lean4

theorem hammingDist_smul_le_hammingDist [∀ i, SMul α (β i)] {k : α} {x y : ∀ i, β i} :
    hammingDist (k • x) (k • y) ≤ hammingDist x y :=
  hammingDist_comp_le_hammingDist fun i => (k • · : β i → β i)

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