English
Given lists l of indices and functions f,g with a relation r on their products, if r(1,1) holds and r is preserved by left-multiplication by f i and g i, then r holds for the products of the mapped lists.
Русский
Даны списки индексов и функции f,g с отношением r на их произведениях; если r(1,1) верно и r сохраняется при левом умножении на f i и g i, то r выполняется для произведений соответствующих отображённых списков.
LaTeX
$$$r\ 1\ 1 \to (\forall i, r a b \to r (f i * a) (g i * b)) \to r ( (l.map f).prod ) ( (l.map g).prod )$$$
Lean4
@[to_additive]
theorem prod_hom_rel (l : List ι) {r : M → N → Prop} {f : ι → M} {g : ι → N} (h₁ : r 1 1)
(h₂ : ∀ ⦃i a b⦄, r a b → r (f i * a) (g i * b)) : r (l.map f).prod (l.map g).prod :=
List.recOn l h₁ fun a l hl => by simp only [map_cons, prod_cons, h₂ hl]
