Theorems · Theorem · order theory

monovary_iff_forall_smul_nonneg

∀ {ι : 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 : ι → β}, Monovary f g ↔ ∀ (i j : ι), 0 ≤ (f j - f i) • (g j - g i)

Defined in

Mathlib.Algebra.Order.Monovary

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingLinearOrderIsStrictOrderedRingAddCommGroupLinearOrderIsOrderedAddMonoidModuleIsStrictOrderedModule