English
If r is a relation on M,N with r 1 1 and h₂ preserves r under multiplication by fixed a, then r holds for the pair of products after mapping by f and g.
Русский
Если r — отношение на M,N с r 1 1 и если r сохраняется при умножении на фиксированное a слева, тогда r выполняется для пар произведений после отображения f и g.
LaTeX
$$$\\forall s: \\mathrm{Multiset}\\; ι, \\; r 1 1 \\rightarrow (\\forall a b c, r b c \\rightarrow r (f a \\cdot b) (g a \\cdot c)) \\rightarrow r (\\mathrm{map} f s).prod (\\mathrm{map} g s).prod$$
Lean4
@[to_additive]
theorem prod_hom_rel (s : Multiset ι) {r : M → N → Prop} {f : ι → M} {g : ι → N} (h₁ : r 1 1)
(h₂ : ∀ ⦃a b c⦄, r b c → r (f a * b) (g a * c)) : r (s.map f).prod (s.map g).prod :=
Quotient.inductionOn s fun l => by simp only [l.prod_hom_rel h₁ h₂, quot_mk_to_coe, map_coe, prod_coe]
