English
The product over Ico(m,n) times the product over Ico(n,k) equals the product over Ico(m,k): ∏_{i∈Ico(m,n)} f(i) · ∏_{i∈Ico(n,k)} f(i) = ∏_{i∈Ico(m,k)} f(i).
Русский
Произведение по Ico(m,n) и по Ico(n,k) равно произведению по Ico(m,k): ∏ f(i) на Ico(m,n) · ∏ f(i) на Ico(n,k) = ∏ f(i) на Ico(m,k).
LaTeX
$$$$ \\displaystyle \\left(\\prod_{i \\in \\mathrm{Ico}(m,n)} f(i)\\right) \\left(\\prod_{i \\in \\mathrm{Ico}(n,k)} f(i)\\right) = \\prod_{i \\in \\mathrm{Ico}(m,k)} f(i). $$$$
Lean4
@[to_additive]
theorem prod_Ico_consecutive (f : ℕ → M) {m n k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) :
((∏ i ∈ Ico m n, f i) * ∏ i ∈ Ico n k, f i) = ∏ i ∈ Ico m k, f i :=
Ico_union_Ico_eq_Ico hmn hnk ▸ Eq.symm (prod_union (Ico_disjoint_Ico_consecutive m n k))
