English
If l1 is a sublist of l2 with respect to Forall₂ ≤, then l1.prod ≤ l2.prod provided that all elements of l2 are at least 1.
Русский
Если l1 — подсписок l2 по отношению Forall₂ ≤, тогда l1.prod ≤ l2.prod при условии, что все элементы l2 не менее 1.
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
/-- If `l₁` is a sublist of `l₂` and all elements of `l₂` are greater than or equal to one, then
`l₁.prod ≤ l₂.prod`. One can prove a stronger version assuming `∀ a ∈ l₂.diff l₁, 1 ≤ a` instead
of `∀ a ∈ l₂, 1 ≤ a` but this lemma is not yet in `mathlib`. -/
@[to_additive sum_le_sum /-- If `l₁` is a sublist of `l₂` and all elements of `l₂` are nonnegative,
then `l₁.sum ≤ l₂.sum`.
One can prove a stronger version assuming `∀ a ∈ l₂.diff l₁, 0 ≤ a` instead of `∀ a ∈ l₂, 0 ≤ a`
but this lemma is not yet in `mathlib`. -/
]
theorem prod_le_prod' [Preorder M] [MulRightMono M] [MulLeftMono M] {l₁ l₂ : List M} (h : l₁ <+ l₂)
(h₁ : ∀ a ∈ l₂, (1 : M) ≤ a) : l₁.prod ≤ l₂.prod := by
induction h with
| slnil => rfl
| cons a _ ih' =>
simp only [prod_cons, forall_mem_cons] at h₁ ⊢
exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)
| cons₂ a _ ih' =>
simp only [prod_cons, forall_mem_cons] at h₁ ⊢
exact mul_le_mul_left' (ih' h₁.2) _
