Theorems · Theorem · order theory

StrictMono.smul_const

∀ {α : Type u_1} {β : Type u_2} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero β]
  [SMulPosStrictMono α β] {γ : Type u_3} [inst_5 : Preorder γ] {f : γ → α},
  StrictMono f → 0 < b → StrictMono fun x => f x • b

Scalar multiplication on the right by a positive element preserves strict monotonicity.

Defined in

Mathlib.Algebra.Order.Module.Defs

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

SMulPreorderPreorderZeroSMulPosStrictMonoPreorder