hammingDist_comp — Mathlib

English

If each coordinate map f_i is injective, then applying f_i coordinate-wise preserves the exact Hamming distance.

Русский

Если каждое отображение f_i инъективно, то по координатам применение f_i сохраняет точное расстояние Хэмминга.

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 (f : ∀ i, γ i → β i) {x y : ∀ i, γ i} (hf : ∀ i, Injective (f i)) :
    (hammingDist (fun i => f i (x i)) fun i => f i (y i)) = hammingDist x y :=
  le_antisymm (hammingDist_comp_le_hammingDist _) <| card_mono (monotone_filter_right _ fun i H1 H2 => H1 <| hf i H2)

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