eventually_constant_prod — Mathlib

English

If a sequence u(n) stabilizes to 1 from some index N onward (u(n) = 1 for all n ≥ N), then the product over range n equals the product over range N for any n ≥ N.

Русский

Если последовательность u(n) становится равной 1 после некоторого индекса N, то произведение по диапазону n равно произведению по диапазону N для любого n ≥ N.

LaTeX

$$$\exists N,\\(\forall n \ge N, u(n) = 1) \implies (\forall n \ge N, \prod_{k=0}^{n-1} u(k) = \prod_{k=0}^{N-1} u(k))$$$

Lean4

@[to_additive]
theorem eventually_constant_prod {u : ℕ → M} {N : ℕ} (hu : ∀ n ≥ N, u n = 1) {n : ℕ} (hn : N ≤ n) :
    (∏ k ∈ range n, u k) = ∏ k ∈ range N, u k :=
  by
  obtain ⟨m, rfl : n = N + m⟩ := Nat.exists_eq_add_of_le hn
  clear hn
  induction m with
  | zero => simp
  | succ m hm => simp [← add_assoc, prod_range_succ, hm, hu]

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