prod_Ioc_succ_top — Mathlib

English

For natural indices, extending the upper end of Ioc by one adds one more factor: ∏_{k∈Ioc(a,b+1)} f(k) = (∏_{k∈Ioc(a,b)} f(k)) · f(b+1).

Русский

Для натуральных индексов: расширение верхнего конца Ioc на единицу добавляет ещё один множитель: ∏ f(k) по Ioc(a,b+1) = (∏ f(k) по Ioc(a,b)) · f(b+1).

LaTeX

$$$$ \\displaystyle \\prod_{k \\in \\mathrm{Ioc}(a,b+1)} f(k) = \\left(\\prod_{k \\in \\mathrm{Ioc}(a,b)} f(k)\\right) \\cdot f(b+1). $$$$

Lean4

@[to_additive]
theorem prod_Ioc_succ_top {a b : ℕ} (hab : a ≤ b) (f : ℕ → M) :
    (∏ k ∈ Ioc a (b + 1), f k) = (∏ k ∈ Ioc a b, f k) * f (b + 1) := by
  rw [← prod_Ioc_consecutive _ hab (Nat.le_succ b), Nat.Ioc_succ_singleton, prod_singleton]

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