monotone_prod_take — Mathlib

English

For any finite list L of a commutative monoid M with canonical order, the function i ↦ (L.take i).prod is monotone nondecreasing in i.

Русский

Для любого конечного списка L в коммутативном моноиде M с каноническим порядком функция i ↦ (L.take i).prod монотонно возрастает по i.

LaTeX

$$$\\forall L:\\,\\text{List } M,\\ Monotone (\\lambda i. (L.take i).prod).$$

Lean4

@[to_additive]
theorem monotone_prod_take (L : List M) : Monotone fun i => (L.take i).prod :=
  by
  refine monotone_nat_of_le_succ fun n => ?_
  rcases lt_or_ge n L.length with h | h
  · rw [prod_take_succ _ _ h]
    exact le_self_mul
  · simp [take_of_length_le h, take_of_length_le (le_trans h (Nat.le_succ _))]

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