Theorems · Theorem · order theory

List.prod_map_lt_prod_map

∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R]
  [NeZero 1] {ι : Type u_2} {s : List ι},
  s ≠ [] → ∀ (f g : ι → R), (∀ i ∈ s, 0 < f i) → (∀ i ∈ s, f i < g i) → (List.map f s).prod < (List.map g s).prod

Defined in

Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Cited by

1 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidWithZeroPartialOrderZeroLEOneClassPosMulStrictMonoNeZero