prod_le_prod' — Mathlib

English

Alternative presentation of SublistForall₂.prod_le_prod' under similar assumptions.

Русский

Альтернатива формулировки 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₁ l₂ : List M} (h : SublistForall₂ (· ≤ ·) l₁ l₂)
    (h₁ : ∀ a ∈ l₂, (1 : M) ≤ a) : l₁.prod ≤ l₂.prod :=
  let ⟨_, hall, hsub⟩ := sublistForall₂_iff.1 h
  hall.prod_le_prod'.trans <| hsub.prod_le_prod' h₁

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