English
Let f and g be index-wise functions taking values in a ordered commutative monoid, and let a1, a2 be the HasProd values of f and g with respect to a summation filter L. If f ≤ g pointwise and L is nontrivial, then a1 ≤ a2.
Русский
Пусть f и g — функции с индексами, принимающие значения в упорядоченном коммутативном моноиде, и пусть a1, a2 — значения произведений HasProd(f) и HasProd(g) относительно фильтра суммирования L. Если f ≤ g по каждому индексу и L не тривиален, то a1 ≤ a2.
LaTeX
$$$\\forall f,g,a_1,a_2:\\, \\text{HasProd } f\, a_1\, L \\to \\text{HasProd } g\, a_2\, L \\to (f \\le g) \\to a_1 \\le a_2$$$
Lean4
@[to_additive]
theorem hasProd_mono (hf : HasProd f a₁ L) (hg : HasProd g a₂ L) (h : f ≤ g) [L.NeBot] : a₁ ≤ a₂ :=
hasProd_le h hf hg
