hammingDist_comp_le_hammingDist — Mathlib

English

Applying coordinate-wise injective maps does not increase the Hamming distance.

Русский

Позиционно-координатное отображение, каждое отображение инъективное, не увеличивает расстояние Хэмминга.

LaTeX

$$hammingDist( (i => f_i(x_i)) , (i => f_i(y_i)) ) ≤ hammingDist(x,y) \text{ if } ∀ i, Injective(f_i)$$

Lean4

theorem hammingDist_comp_le_hammingDist (f : ∀ i, γ i → β i) {x y : ∀ i, γ i} :
    (hammingDist (fun i => f i (x i)) fun i => f i (y i)) ≤ hammingDist x y :=
  card_mono (monotone_filter_right _ fun i H1 H2 => H1 <| congr_arg (f i) H2)

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