Theorems · Theorem · order theory

MonovaryOn.smul_add_smul_le_smul_add_smul

∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [IsStrictOrderedModule α β] {f : ι → α} {g : ι → β} {s : Set ι},
  MonovaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g j + f j • g i ≤ f i • g i + f j • g j

Alias of the forward direction of monovaryOn_iff_smul_rearrangement. Two functions monovary iff the rearrangement inequality holds.

Defined in

Mathlib.Algebra.Order.Monovary

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingLinearOrderIsStrictOrderedRingAddCommGroupLinearOrderIsOrderedAddMonoidModuleIsStrictOrderedModule