Theorems · Theorem · order theory

StrictMonoOn.neg

∀ {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst_1 : Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α]
  [inst_4 : Preorder β] {f : β → α} {s : Set β}, StrictMonoOn f s → StrictAntiOn (fun x => -f x) s

Defined in

Mathlib.Algebra.Order.Group.Unbundled.Basic

Cited by

3 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext

Assumes

AddGroupPreorderAddLeftStrictMonoAddRightStrictMonoPreorder