prod_le_prod' — Mathlib

English

Another framing of SublistForall₂.prod_le_prod' as above.

Русский

Другая формулировка prod_le_prod' для SublistForall₂.

LaTeX

$$[Preorder M] [MulRightMono M] [MulLeftMono M] {l1 l2 : List M} (h : SublistForall₂ (≤) l1 l2) (h1 : ∀ a ∈ l2, 1 ≤ a) : l1.prod ≤ l2.prod$$

Lean4

@[to_additive sum_le_sum]
theorem prod_le_prod' [Preorder M] [MulRightMono M] [MulLeftMono M] {l : List ι} {f g : ι → M}
    (h : ∀ i ∈ l, f i ≤ g i) : (l.map f).prod ≤ (l.map g).prod :=
  Forall₂.prod_le_prod' <| by simpa

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