Theorems · Theorem · order theory

Antitone.const_mul_of_nonpos

∀ {R : Type u} {α : Type u_1} [inst : Semiring R] [inst_1 : Preorder R] {a : R} [inst_2 : Preorder α] {f : α → R}
  [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R],
  Antitone f → a ≤ 0 → Monotone fun x => a * f x

Defined in

Mathlib.Algebra.Order.Ring.Unbundled.Basic

Cited by

0 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms

Assumes

SemiringPreorderPreorderExistsAddOfLEPosMulMonoAddRightMonoAddRightReflectLE