English
If for all i in a finite index set s we have f(i) ~ᵤ g(i), then the products over s are also associated: (∏ i∈s f(i)) ~ᵤ (∏ i∈s g(i)).
Русский
Если для каждого i в конечном индексе s элементы f(i) ассоциированы с g(i), то их произведения по i также ассоциированы.
LaTeX
$$∀ i ∈ s, f(i) ~ᵤ g(i) → (∏ i∈s f(i)) ~ᵤ (∏ i∈s g(i))$$
Lean4
theorem prod {M : Type*} [CommMonoid M] {ι : Type*} (s : Finset ι) (f : ι → M) (g : ι → M)
(h : ∀ i, i ∈ s → (f i) ~ᵤ (g i)) : (∏ i ∈ s, f i) ~ᵤ (∏ i ∈ s, g i) := by
induction s using Finset.induction with
| empty =>
simp only [Finset.prod_empty]
rfl
| insert j s hjs IH =>
classical
convert_to (∏ i ∈ insert j s, f i) ~ᵤ (∏ i ∈ insert j s, g i)
rw [Finset.prod_insert hjs, Finset.prod_insert hjs]
grind [Associated.mul_mul]
