English
If k runs over a finite set F and each g(k) lies in A(i(k)), then the product ∏_{k∈F} g(k) lies in A(∑_{k∈F} i(k)).
Русский
Если сумма элементов по конечному набору F даёт градацию i(k), и каждый g(k) принадлежит соответствующей компоненте, то произведение ∏ g(k) принадлежит компоненте A(∑ i(k)).
LaTeX
$$$ \forall F \ :\ Finset\ κ ,\ (\forall k ∈ F, g(k) ∈ A(i(k))) \Rightarrow \prod_{k ∈ F} g(k) ∈ A\Big(\sum_{k ∈ F} i(k)\Big) $$$
Lean4
theorem prod_mem_graded (hF : ∀ k ∈ F, g k ∈ A (i k)) : ∏ k ∈ F, g k ∈ A (∑ k ∈ F, i k) := by
classical
induction F using Finset.induction_on
· simp [GradedOne.one_mem]
·
case insert j F' hF2 h3 =>
rw [Finset.prod_insert hF2, Finset.sum_insert hF2]
apply SetLike.mul_mem_graded (by grind)
grind
