prod_le_prod_of_rel_le — Mathlib

English

If a relation Rel(≤) orders multisets s ≤ t, then s.prod ≤ t.prod.

Русский

Если s ≤ t по отношению Rel(≤), то произведение s не превышает произведение t.

LaTeX

$$$ s \; \mathrm{Rel}_{(\le)} \; t \Rightarrow s.prod \le t.prod $$$

Lean4

@[to_additive]
theorem prod_le_prod_of_rel_le [MulLeftMono α] (h : s.Rel (· ≤ ·) t) : s.prod ≤ t.prod := by
  induction h with
  | zero => rfl
  | cons rh _ rt =>
    rw [prod_cons, prod_cons]
    exact mul_le_mul' rh rt

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