Theorems · Theorem · order theory

strictAnti_of_odd_strictAntiOn_nonneg

∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G]
  [inst_3 : AddCommGroup H] [inst_4 : PartialOrder H] [IsOrderedAddMonoid H] {f : G → H},
  (∀ (x : G), f (-x) = -f x) → StrictAntiOn f (Set.Ici 0) → StrictAnti f

An odd function on a linear ordered additive commutative group is strictly antitone on the whole group provided that it is strictly antitone on Set.Ici 0.

Defined in

Mathlib.Order.Monotone.Odd

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidAddCommGroupPartialOrderIsOrderedAddMonoid