English
If each f_i is injective and f_i(0) = 0, then the Hamming norm is preserved under composition: hammingNorm(i ↦ f_i(x_i)) = hammingNorm(x).
Русский
Если каждая f_i инъективна и f_i(0) = 0, то норма Хэмминга сохраняется при композиции: hammingNorm(i ↦ f_i(x_i)) = hammingNorm(x).
LaTeX
$$$\forall i, \mathrm{Injective}(f_i) \Rightarrow \mathrm{hammingNorm}(i \mapsto f(i, x_i)) = \mathrm{hammingNorm}(x)$$$
Lean4
theorem hammingNorm_comp (f : ∀ i, γ i → β i) {x : ∀ i, γ i} (hf₁ : ∀ i, Injective (f i)) (hf₂ : ∀ i, f i 0 = 0) :
(hammingNorm fun i => f i (x i)) = hammingNorm x := by
simpa only [← hammingDist_zero_right, hf₂] using hammingDist_comp f hf₁ (y := fun _ ↦ 0)
