English
Similarly for Ioc, the product over Ioc(m,n) times the product over Ioc(n,k) equals the product over Ioc(m,k): ∏_{i∈Ioc(m,n)} f(i) · ∏_{i∈Ioc(n,k)} f(i) = ∏_{i∈Ioc(m,k)} f(i).
Русский
Аналогично для Ioc: произведение по Ioc(m,n) и Ioc(n,k) равно Ioc(m,k).
LaTeX
$$$$ \\displaystyle \\left(\\prod_{i \\in \\mathrm{Ioc}(m,n)} f(i)\\right) \\left(\\prod_{i \\in \\mathrm{Ioc}(n,k)} f(i)\\right) = \\prod_{i \\in \\mathrm{Ioc}(m,k)} f(i). $$$$
Lean4
@[to_additive]
theorem prod_Ioc_consecutive (f : ℕ → M) {m n k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) :
((∏ i ∈ Ioc m n, f i) * ∏ i ∈ Ioc n k, f i) = ∏ i ∈ Ioc m k, f i :=
by
rw [← Ioc_union_Ioc_eq_Ioc hmn hnk, prod_union]
apply disjoint_left.2 fun x hx h'x => _
intro x hx h'x
exact lt_irrefl _ ((mem_Ioc.1 h'x).1.trans_le (mem_Ioc.1 hx).2)
