prod_hom_rel — Mathlib

English

If a relation r on M is preserved by multiplication with a fixed 1 and by multiplying corresponding factors, then the relation holds for the products: r(∏ f) (∏ g).

Русский

Если отношение r на M сохраняется под умножением на единицу и по соответствующим множителям, то оно сохраняется и для произведений.

LaTeX

$$$\\forall r\\; (r\\,1\\,1)\\; (h_1\\;h_2):\\; r(\\prod_{x∈s} f x) (\\prod_{x∈s} g x)$$$

Lean4

@[to_additive]
theorem prod_hom_rel [CommMonoid N] {r : M → N → Prop} {f : ι → M} {g : ι → N} {s : Finset ι} (h₁ : r 1 1)
    (h₂ : ∀ a b c, r b c → r (f a * b) (g a * c)) : r (∏ x ∈ s, f x) (∏ x ∈ s, g x) :=
  by
  delta Finset.prod
  apply Multiset.prod_hom_rel <;> assumption

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