prod_le_prod — Mathlib

English

If p ≤ q in Multiset of Associates M, then p.prod ≤ q.prod in the Associated preorder.

Русский

Если p ≤ q в множестве Multiset M, тогда p.prod ≤ q.prod в предожидаемом порядке.

LaTeX

$$Multiset.instPartialOrder.le p q → Associates.instPreorder.le p.prod q.prod$$

Lean4

theorem prod_le_prod {p q : Multiset (Associates M)} (h : p ≤ q) : p.prod ≤ q.prod :=
  by
  haveI := Classical.decEq (Associates M)
  suffices p.prod ≤ (p + (q - p)).prod by rwa [add_tsub_cancel_of_le h] at this
  suffices p.prod * 1 ≤ p.prod * (q - p).prod by simpa
  exact mul_mono (le_refl p.prod) one_le

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