Theorems · Theorem · order theory

StrictAntiOn.neg

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

Defined in

Mathlib.Algebra.Order.Group.Unbundled.Basic

Cited by

4 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext

Assumes

AddGroupPreorderAddLeftStrictMonoAddRightStrictMonoPreorder