prod_le_prod' — Mathlib

English

If l1 and l2 are related by Forall₂ ≤, then (l1.prod) ≤ (l2.prod) given appropriate Monoid structure and 1 ≤ a for all a ∈ l2.

Русский

Если элементы списков связаны через Forall₂ ≤, то произведение левого списка не больше произведения правого при соответствующей структуре монадных операций и условии 1 ≤ a для всех a∈l2.

LaTeX

$$[Preorder M] [MulRightMono M] [MulLeftMono M] {l1 l2 : List M} (h : Forall₂ (≤) l1 l2) : 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 : Forall₂ (· ≤ ·) l₁ l₂) :
    l₁.prod ≤ l₂.prod := by
  induction h with
  | nil => rfl
  | cons hab ih ih' => simpa only [prod_cons] using mul_le_mul' hab ih'

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